Ownership Types
A type system can encode a resource protocol: who is responsible for a value, who may read it, who may write it, and when it must be released. The invariant that makes the proof work is aliasing XOR mutability — and it buys thread safety as a side effect.
How can a compiler prove memory safety with no garbage collector and no runtime check?
The type of a value carries more than its shape: it carries who owns it, whether the current binding is an owner or a borrow, and whether that borrow is shared or unique. The checker maintains these as per-program-point facts over the control-flow graph, which is why this is a data-flow analysis rather than a syntactic rule — the same variable is owned, moved-from, or borrowed at different points in the same function.
The invariant the whole proof rests on: at any program point, a value has either any number of shared references or exactly one mutable reference, never both. A function signature, a transformation or an unsafe block may violate it internally only if it restores the invariant before any checked code can observe the difference — that restoration obligation is precisely what an unsafe block is a promise about, and nothing verifies it.
Key points
- An ownership type system encodes a resource protocol in types: one owner, moves transfer responsibility, drops release, borrows lend temporarily.
- The load-bearing invariant is aliasing XOR mutability — many shared references or one mutable reference, never both.
- Use-after-free, double-free, iterator invalidation and data races are all consequences of that one rule being enforced, not four separate features.
- The technique is not specific to memory: locks, files, transactions and connections are protocols with the same shape and are enforced the same way.
- Moves make copying explicit and let an API consume its receiver, which is how a type-level state machine is built.
- The system is affine rather than linear: a value may be used at most once, and may simply be dropped.
- The rule rejects correct programs — anything genuinely needing aliased mutation — so an audited escape hatch is required, and that is where the residual risk lives.
A type system can encode a protocol
Most type systems answer "what shape is this value". Ownership systems answer a different question: "what is this code allowed to do with it, and when does the responsibility end". That is a protocol, and encoding a protocol in types is a general technique that memory is only the most famous application of.
The building blocks are small. A value has exactly one owner. Assigning or passing it *moves* the ownership, after which the original binding is no longer usable. When the owner goes out of scope the value is released. And instead of moving, you may lend a reference — a borrow — which is valid for a bounded region and does not transfer responsibility.
What makes this a type system rather than a convention is that "no longer usable" is checked. A use of a moved-from binding is a compile error, in the same way that adding a string to a function is a compile error. The system is *affine*: a value may be used at most once as an owner, which is the linear-types family with the "must be used" obligation relaxed to "may be dropped".
And once you see it as a protocol encoding, the applications beyond memory are obvious. A file handle that must be closed, a lock guard that must be released, a database transaction that must be committed or rolled back, a socket that must not be written after shutdown — all of them are protocols, and all of them can be enforced by making the handle an owned value whose destructor performs the release. That is why Rust's MutexGuard needs no discipline from the programmer: forgetting to unlock is not something the API permits you to express.
1let data = Mutex::new(vec![1, 2, 3]);2 3{4 let mut guard = data.lock().unwrap(); // guard OWNS the locked state5 guard.push(4);6} // guard dropped here: unlock happens, always7 8// The protocol is enforced by construction:9// - you cannot touch the Vec without holding the guard10// - you cannot hold the guard without having locked11// - you cannot forget to unlock, because dropping is what unlocks12// - you cannot use the guard after the scope, because it was droppedNo runtime check enforces any of these four. Each is a consequence of the guard being an owned value with a destructor, which is the same machinery that manages heap memory.
Aliasing XOR mutability: why the proof goes through
The rule that makes the whole thing work is a single restriction: you may have many readers, or one writer, never both at once. Every hard guarantee in the system is a consequence of it, and it is worth seeing why rather than memorising it.
Consider the classic use-after-free. It requires a pointer to a value that has been released. Under the rule, releasing happens when the owner is dropped, and the owner cannot be dropped while a borrow of it is live — because the borrow's region would then extend past the owner's lifetime, which the checker rejects. So the dangling pointer has no way to come into existence. [[lifetime-analysis]] is the machinery that decides "is live".
Consider iterator invalidation. You hold an iterator over a collection — a shared borrow — and then push to the collection, which requires a mutable borrow. Two borrows, one of them mutable, at the same time: rejected. In C++ this is undefined behavior discovered at runtime, if at all.
Consider a data race. A data race requires two threads accessing the same location, at least one writing, without synchronisation. The rule forbids a mutable reference to coexist with any other reference at all, so within a thread the situation cannot arise; the marker traits that decide what may cross a thread boundary extend the same reasoning across threads. This is the sense in which ownership buys thread safety for free — the rule was never about memory specifically. Data races and shared mutable state, in the Concurrency domain, are what is being ruled out.
Notice what the rule costs. Perfectly correct programs are rejected: a doubly linked list, a graph with back-references, an observer registry, a cache with entries pointing at each other. All of them need aliasing and mutation together. The system's answer is that those patterns must be built with interior mutability and a runtime check, or inside unsafe with the invariant maintained by hand — which is an honest admission that the rule is stricter than necessary and the compiler cannot tell which cases are the safe ones.
| Approach | When the cost is paid | What it catches | What it cannot do |
|---|---|---|---|
| Manual (C, C++ raw) | Never, by the machine | Nothing. Errors are undefined behavior. | Give any guarantee at all without external tooling. |
| Tracing GC | At runtime, in pauses proportional to the live set | Use-after-free and double-free, completely | Handle non-memory resources; bound pause time without effort |
| Reference counting | At runtime, on every share and release | Use-after-free, given no cycles | Reclaim cycles; avoid atomic traffic when shared across threads |
| Ownership types | At compile time, in rejected programs and annotation effort | Use-after-free, double-free, iterator invalidation, data races | Express cyclic or aliased-mutable structures without an escape hatch |
Moves, and what "affine" buys
Assignment in an ownership system is a move by default: let b = a; transfers responsibility, and a is thereafter unusable. That single decision has consequences that reach much further than memory management.
It makes double-free impossible by construction, because there is only ever one owner to run the destructor. It makes a copy explicit — if you want two, you say clone(), and the cost is visible in the source rather than hidden in an assignment. And it turns "this handle has been consumed" into a type-level fact, which is what lets an API express a state machine: a method that takes self by value consumes the receiver, so the compiler will not let you call it twice or use the old state afterwards.
That last pattern is the typestate idea, and it generalises well beyond Rust. A builder whose build(self) consumes the builder cannot be built twice. A connection whose close(self) consumes it cannot be written to afterwards. A transaction with commit(self) and rollback(self) forces exactly one of them and forbids using the transaction after either. Each of these is an API-design technique available in any language with affine types, and each removes a class of misuse that documentation would otherwise have to warn about — the same argument API state-machine design makes for protocols in general.
The word affine matters: a linear type must be used exactly once, an affine type at most once. Ownership systems are affine because a value may simply be dropped, which is what makes them usable — a linear system would force every value to be explicitly consumed, which is correct and intolerable.
Where the escape hatch is, and what it means
unsafe permits, what the borrow checker accepts — are Rust's and have changed substantially across editions.No ownership system can express every safe program, so all of them have an escape hatch. In Rust it is unsafe, which does not disable the checker but permits five specific operations the checker cannot verify — dereferencing a raw pointer, calling an unsafe function, and so on. The obligation is transferred: inside the block, the invariants are yours to maintain, and the safe code around it is sound *conditional* on your having maintained them.
This is a genuinely better position than an unchecked hole in a type system, and it is worth being precise about why. The obligation is localised — you can enumerate the blocks. It is greppable, so it can be reviewed and audited. And the safe/unsafe boundary is where a library gets to define its own abstraction: Vec is implemented with raw pointers, and the safe API it exposes is sound because a human proved the internals uphold the rule. The entire standard library is an argument of this shape.
It is also worse than no hole, in the ways that always apply to human obligations. The proof is not checked. It can be invalidated by a refactor elsewhere. It relies on the author having understood the exact rules — and the rules for what raw pointers may do are subtle enough that the community maintains a separate reference for them and a dynamic checker to test against.
The transferable lesson is not about Rust. It is that a compile-time proof of a resource protocol is possible, is affordable, is stricter than necessary, and needs an audited escape hatch to be usable — and that the escape hatch is where the residual risk lives. [[type-soundness]] is where that conditional-soundness argument is made in general; [[rust-pipeline]] is where the language is treated as a language.
How it works
The steps, in the order the compiler takes them.
- Each binding is tracked through the control-flow graph with a state: owned, moved-from, borrowed shared, or borrowed mutably.
- A move updates the source binding to moved-from; any later use of it is an error, and at a control-flow merge the state is the join, so a value moved on one path is moved-from afterwards.
- Taking a borrow records a region over which the reference must stay valid; taking a second borrow checks it against the outstanding set for a conflict under the exclusivity rule.
- Dropping an owner is inserted by the compiler at the end of its scope, and is rejected if any borrow of it is still live at that point.
- Function signatures carry the ownership and borrow structure, so the check is modular: a call is checked against the signature without looking inside the callee — which is what makes lifetimes appear in signatures at all.
- Marker traits classify which types may be moved to another thread and which may be shared across threads; the compiler derives them structurally, so thread safety follows from the same facts.
- An
unsafeblock permits a fixed set of otherwise forbidden operations; the checker continues to run on everything else, and the block's obligations are recorded nowhere and verified by nothing.
How it breaks
What the engineer observes when it goes wrong — not what goes wrong internally.
- A program that is obviously correct is rejected — a struct holding two references into the same collection, a parent pointer in a tree — and the engineer restructures the data rather than the logic, sometimes for the better and sometimes not.
- The escape hatch is used to get past a borrow error, the invariant is not actually upheld, and the resulting corruption appears as a wrong value in unrelated code with no fault at the site of the error.
- A resource protocol is expressed with a guard type, and someone binds the guard to
_instead of a name, which drops it immediately; the lock is released at once and the critical section runs unprotected with nothing reporting it. - An
unsafeblock that was correct when written is invalidated by a change to a caller months later; nothing rechecks it, and the failure surfaces as memory corruption under load. - Interior mutability is reached for to escape the exclusivity rule, moving the check to runtime; the program now panics on a borrow conflict in production instead of failing to compile.
- A team reads compile errors as the compiler being obstructive, adds clone calls everywhere to make them go away, and ships a program that is correct and allocates several times more than it needs to.
When it helps
- Systems code where a garbage collector is unacceptable — kernels, embedded targets, real-time paths, allocators — and manual management is the alternative.
- Any resource with a release obligation: locks, file handles, sockets, transactions, GPU buffers, FFI handles.
- Concurrent code, where the same invariant that prevents aliasing bugs also rules out data races within the checked region.
- API design generally: consuming methods turn protocol violations into compile errors, which is available as a technique wherever affine types are.
When it hurts
- Inherently aliased-and-mutable structures: graphs with back-edges, doubly linked lists, observer registries, caches with cross-references. All are expressible and none is pleasant.
- Rapid prototyping, where the annotation and restructuring effort is paid up front and the program may not survive the week.
- Teams without the invariant in their heads, where the compiler errors read as arbitrary and the learned response is to clone or to reach for the escape hatch.
- Code that must interoperate heavily with a C API, where the ownership story on the other side is documentation at best and the boundary is necessarily unsafe.
What it costs
Every one of these is paid by something.
- Compile-time proof buys the elimination of an entire class of memory and concurrency errors with no runtime check, and pays by rejecting correct programs — the rule is stricter than necessary and the compiler cannot tell which rejections are the safe ones.
- Moves by default buy the impossibility of double-free and make copies visible in the source, and pay in ergonomics: ordinary assignment now has consequences, and code that reads naturally in other languages must be restructured.
- Lifetimes in signatures buy modular checking — a call is verified against a signature without inspecting the body — and pay by putting the analysis into the public API, so a lifetime change is a breaking change.
- An escape hatch buys the ability to implement the abstractions the rule forbids, and pays by making the soundness claim conditional on human obligations that nothing verifies and that a distant refactor can invalidate.
What else you could do
What a different compiler or language does instead, and when that is better.
- Tracing garbage collection removes the question entirely for memory, at the cost of pauses, throughput overhead and no help whatsoever with locks, files or transactions — and the compiler-side half of a collector — safepoints, stack maps, write barriers — is a separate subject.
- Reference counting gives deterministic release with no static analysis, at the cost of per-operation counter traffic, atomic operations when shared across threads, and leaked cycles.
- Region-based allocation ties lifetimes to a scope and frees everything at once, which is simpler and much less precise — excellent for arena-shaped workloads such as a compiler pass and wrong for long-lived object graphs.
- RAII without ownership checking, as in C++, gives the same destructor-based release protocol with none of the aliasing guarantees: the pattern is available and use-after-free remains possible.
- Static analysis bolted onto an unsafe language — sanitizers, model checkers, ownership annotations checked by a linter — catches much of it without a language change, at the cost of being unsound, incomplete, or both.
See it for yourself
The flag, dump or tool that shows you this directly.
cargo buildis the primary tool: the borrow checker's errors name the conflicting borrows and their regions, and reading them as a description of the invariant rather than as an obstacle is most of the learning curve.rustc -Z dump-mir=all(nightly) shows the MIR the borrow checker actually analyses, including the compiler-inserted drops — which is where "why is this dropped here" questions get answered.cargo miri testinterprets the program and checks the aliasing rules dynamically, which is the way to test whether anunsafeblock actually upholds what it promised.grep -rn "unsafe" src/is the audit. The count and the location of unsafe blocks is the honest measure of how much of a codebase's safety is proved versus asserted.- For the protocol-encoding technique specifically, look at any guard type's
Dropimplementation — that is the whole mechanism, and it is usually five lines.
Plausible wrong readings
Stated the way a confident engineer states them.
- "The borrow checker prevents memory leaks." It does not, and leaking is explicitly safe. A reference cycle under reference counting leaks with the checker entirely satisfied; what is prevented is use-after-free, not failure to free.
- "Ownership is about memory." Memory is the flagship application. The mechanism is a resource protocol encoded in types, and locks, files and transactions use exactly the same machinery.
- "If it compiles, it is correct." It is free of one class of error, in the checked region, conditional on every
unsafeblock having upheld its obligations. Logic errors, deadlocks and leaks are all untouched. - "The compiler is being unnecessarily strict." Frequently it is being strict about a program that happens to be correct, because the rule is a conservative approximation. That is a real cost of the design, not a misunderstanding on your part.
Misconceptions
The claim, and what is actually true.
Go deeper
The same idea at increasing depth. Stop wherever it stops being useful.
overview
Instead of a garbage collector deciding when a value can be freed, the type system tracks who owns it. There is one owner; passing it along transfers ownership; when the owner goes out of scope, the value is released. You can lend out temporary references, subject to one rule: many readers or one writer, never both. Everything the system guarantees follows from that rule being enforced at compile time.
practical
The technique generalises past memory, and that is the part worth taking to other languages. Any resource with a release obligation — a lock, a file, a transaction — becomes safe by being an owned value whose destructor releases it, so forgetting is not expressible. Any protocol with an ordering constraint becomes safe by having methods consume the receiver, so calling twice or calling after close does not type-check. When you hit a borrow error on a genuinely correct program, the useful move is usually to restructure ownership — split the borrow, index instead of holding a reference, or introduce an explicit arena — rather than to clone or to reach for the escape hatch.
advanced
The deep claim is that aliasing-XOR-mutability is not primarily a memory-safety rule; it is a *reasoning* rule, and memory safety is one thing that falls out of it. If a mutable reference is unique, then no other code can observe or modify the value through another path, which means local reasoning about it is valid — and that is exactly the precondition an optimizer needs. This is why the rule pays off three times over: it eliminates aliasing bugs, it eliminates data races, and it hands the compiler a noalias guarantee that C compilers spend enormous effort trying to infer and usually cannot. The same information that makes the program provably safe makes it more optimizable, which is unusual — most safety mechanisms cost performance. The price is that the rule is a conservative approximation, so the programs it rejects include correct ones, and the escape hatch exists because no decidable analysis could tell them apart.
How much this depends on
Nothing in this domain is true of every compiler. These say how much.
unsafe code, FFI boundaries and anything reached through interior mutability with a manual synchronisation story are outside it. The marker traits that carry the guarantee across thread boundaries are derived structurally and can be implemented by hand, which is an unsafe operation for exactly this reason.If you were asked this in an interview
- State the one invariant an ownership system enforces, and derive use-after-free prevention and data-race prevention from it.
- Ownership is usually explained in terms of memory. Give an example where it enforces something that is not memory, and say what makes it work.
- What does an
unsafeblock actually change, and what does its presence do to the soundness claim for the code around it?