How Rust thinks about Soundness

October 2, 2026

I was asked about how we can more thoroughly look at how rust handles memory safety and soundness in the context of Valen. It’s a useful well for language designers to draw from and it’s worth documenting the rough mental model that rust’s design works in. My writing here is pretty off the cuff, and I’ve missed out plenty :) Try to take it as food for thought!

What could be a good way to compare [Valen] and Rust

I think a good way to structure this is explicitly addressing the “precise model” and the “intuitive model” of rust. There are some white lies sometimes taught to rust learners with the intent that it helps them start using the tools faster without information overload, but they’re actually missing detail - the exact rules of interior mutability is a good example.

In writing, you can approach that in a couple ways. Especially, it’s interesting to have a programming language where we don’t need so many white lies to teach it. If a new design allows learners to pick up the rules by accurately being taught the subset of them they need to know, that’s really great.

It’s a large topic to fully cover, but the precise model starts with

• there are intrinsic operations given by the language, which have defined behaviour in some situations, and critically also have situations where their behaviour is undefined. These are our ptr::reads and ptr::writes but also plenty of more niche operations with their own requirements.
• when calling an intrinsic during execution, the call is “sound” if all the requirements are met
  • here we’re thinking soundness like
    • is in bounds
    • has not been freed
    • does not race with an access on another thread
    • has correct noalias annotations
    • ..
  • If a function is sound to call for all well-typed inputs, we call that function “safe”, otherwise it is “unsafe”

(All just foundational definitions there, should be unsurprising)

The important thing to note here is that we have multiple operations that need to be the unique user of a value in a program: when accessing a pointer with a write, it is unsound for another thread to be using that same pointer. This is where the new type system feature comes from, we need the language to be able to tell us “there are no other pointer-typed objects in this program with the same address as this pointer”. That’s enough to meet the soundness requirements of a bunch of primitives.

The second (still very significant) utility is effectively “caching”. We want to be able to implement iterators that capture a pointer, then increment it. This will behave the same as (0..vec.len()).map(|i| vec.as_ptr() + i) as long as the vec’s buffer pointer hasn’t changed. Iow, we haven’t invalidated the cached read of the buffer’s pointer. This is also pragmatically how noalias works: noalias pointers “can be cached” and we know a limited set of operations that invalidate that cache.

So the main role of this new feature is to support tracking this exclusivity. We need that for justifying plenty of low level code patterns. At this point, the design isn’t fixed, we just care about any type signature for functions that can use unique pointer like this.

Rust, then, has a few features:

• normal pointers (mut Vs const is practically a lint), which contain an address and make no real guarantees about what it points to.

  • these can ofc freely alias, and here we’re working on the core intrinsic level: we have primitives with aliasing requirements coming from llvm and the hardware, and if we can ensure writes aren’t racy, we can use these freely

• atomic pointer intrinsics, and types for using them

  • memory that is accessed atomically always needs all other users of that memory to use the atomic intrinsics, which is the main motivation between having dedicated atomic types.
  • and in the low level frame, we can often establish uniqueness with atomics. A ptr_atomic.fetch_add(1) ensures the current thread is the only one in the program that’s going to see that pointer, and it’s enough to use other low level primitives that are sensitive to races. We want a language to be able to support this pattern in high level safe code. (+ Note this is not related to send/sync yet)

• affine types themselves get us started with the high level APIs. With a type that can’t be duplicated, any value you create that was unique at construction will not be duplicated, and code can rely on it being unique later. This gets us Box and enough reason to make safe read+write operations for it.

Sigh. this is rough to summarize well >.>

Cutting it short because it’s late - we then get to exclusive references, which are a tool that the type system gives us to preserve the “there are no other pointer typed objects in this program with the same address” property with an additional “reborrow” operation, allowing copies to be temporarily made to be passed into functions.

Critically, that’s one tool: plenty of other types in rust store pointers with other guarantees, static_rc being a fun example, and some storing graphs that have internal aliasing, but let the caller use a single node exclusively.

The point is that we have plenty of high level patterns supported in the types, for justifying the exact restrictions of the low level operations. For very specifically multi threaded pointer operations, that’s literally “aliasing xor mutability” at the llir level. That’s why AXM is rust’s solution to super-ergonomic multi threading, because it captures the requirements of multi threaded pointers and makes them (relatively) easy to preserve on absolutely everything.

A fun thing to note about this safe multi threading feature - it’s where the “mutable pointer” misnomer comes from. The types are actually tracking aliasing, but when only talking about multi threading in this way where axm is being used, shared <-> immutable and unique <-> mutable is literally true because that’s how xor works :P

This is the framing that leads to group borrowing looking like an extension of the rust mental model: when you’re in the habit of designing types to capture specific aliasing patterns you need, group borrowing is offering support for another bundle of useful patterns

something that deserves more explanation is how reference flattening works: &unique &unique T flattening to &unique T but &shared &unique T only flattening to &shared T is specifically because we’re preserving this uniqueness property. In particular, literal mutability (we could add a new “immutable pointer” type to rust for allowing immutable pages and dedupped memory etc) doesn’t get lost that way. It’s a big part of how libraries compose together well