Rust from the Contract Up

One linearized path that derives Rust from a single promise — safe code has no undefined behavior — and a single budget — no garbage collector, no run-time system, no hidden cost. Every rule you will meet (ownership, moves, borrows, lifetimes, traits, Send and Sync, unsafe) is presented as the move that was forced by the problem the previous rule created, so that by the end the language reads as the only design that was left. The working language is Rust; the transferable skill is asking, of any line in any language, who owns it, who else can reach it, and where the proof stops.

The thesis, in one sentence: where its two companion tracks split the safety contract between the programmer (C++ from the Machine Up trusts you) and the run-time system (Go from the Team Up constrains the program), Rust verifies it: the compiler keeps the contract, at C++'s run-time cost, and the price is paid at compile time, in the shape of your code. The series runs in six movements — the promise, the law (ownership and borrowing), types that carry proofs, when one owner is not enough, the trust boundary, and shipping with an honest bill. Read it straight through, or start at the orientation for the map.

Who this is for

A working programmer who knows some language — Python, Java, Go, C++ — and wants to understand Rust rather than memorize it. No Rust is assumed, and every term (stack, heap, pointer, trait, lifetime) is defined when it first appears. The C++ and Go tracks are companions, not prerequisites: where a lesson touches ground they covered it says so in one line and moves on. By the end you can state the promise and the law; read a borrow-checker error as three points and fix the design instead of fighting the message; choose between an owner, a borrow, an Rc and a RefCell on purpose; write generics, trait objects, closures and iterators and say what each compiles to; reason about Send and Sync; explain what an async fn turns into; and say exactly what an unsafe block promises.

How this track is built

An original first-principles track — not a translation of any book and not a reference manual. Three things set it apart from its two siblings. (1) A relay, not a list. Every lesson opens with the problem the previous one created and closes by creating the next; that hand-off is one sentence, the baton, which appears word for word at the end of one lesson, at the start of the next, and in the table below — a script checks it. (2) Tested code. Every Rust snippet is compiled by the real compiler (rustc 1.98.1, edition 2024) and carries a badge generated from the verdict — compiles, rejected with a given error code, or panics — so "this is rejected with E0502" is a tested fact, and quoted error messages are lines the compiler actually printed. (3) Widgets that compute. Every lesson ships one widget that runs the mechanism the lesson is about — a model of the checker, solver or layout algorithm — rather than drawing a picture of it. Deliberately out of scope: macros beyond derive, no_std and embedded, WebAssembly, and the async ecosystem's crate-level details.

Part I · The promise (lessons 00–02)

Turn a slogan into a specification: what "no undefined behavior" must rule out, and the vocabulary to state it.

Orientation — Rust makes the compiler keep the contract

C++ trusts, Go constrains, Rust verifies. The promise (safe code has no undefined behavior), the budget (no garbage collector, no run-time system, no hidden cost), a design-by-elimination widget that shows why only a static proof is left, the five-question habit, and the 23-lesson chain.

The promise, made precise — seven bugs, one law

Ask what a checker must know. Five undefined-behavior families yield to cheap local rules; use-after-free, double free, iterator invalidation and data races are one hazard — an effect on a place through one name while another live name can reach it. Forbid the overlap: shared XOR exclusive, and see it feed the optimizer.

Places, values, and the stack

The vocabulary the law needs, in the simplest case: no heap and no borrowing. Places and values, immutability by default, the stack frame, slices as pointer-plus-length, definite assignment, defined overflow — the cheap rows of Lesson 01 paid off — and the exact point where the heap forces the real problem.

Part II · Ownership and borrowing — the law (lessons 03–08)

Derive the law that keeps the promise, one forced step at a time: an owner, a move, a borrow, a lifetime, the algorithm that checks them, the signature that makes checking modular.

Ownership — one owner, one drop

Who frees a heap value, exactly once? Make it a language rule: every value has one owner and is dropped when the owner's scope ends. String, Vec and Box as a stack header plus a heap buffer, Drop as RAII made mandatory, drop order, and why this is the C++ unique_ptr with no way to opt out.

Move — assignment as transfer

Copying an owner makes a second owner, so assignment moves: the source is statically dead (E0382). Copy as the opt-out, Clone as the explicit price, functions that take and give back ownership, and why a move copies only the stack header.

Borrowing — the law

Use a value without owning it: &T and &mut T under the one law — many readers or one writer. Reborrowing, auto-deref, moving out of a &mut with take and replace, iterator invalidation as a compile error, and a widget that applies the law to overlapping borrows.

Lifetimes — a borrow is a region

A borrow's lifetime is a region of the program and must fit inside its owner's. Outlives, E0597 and E0515, why lifetimes are erased at run time and cost nothing, and why a collector or a run-time check are the roads not taken.

The borrow checker — liveness on the control-flow graph

What the compiler actually computes: a loan is live from its creation to the last use of anything derived from it, along every path. The three-point anatomy of every error, non-lexical lifetimes, two-phase borrows, and the safe programs it still rejects — with a working mini borrow checker.

Lifetimes in signatures — the modular contract

Checking is per function, so the input-to-output borrow relationship must be written in the signature. Lifetime parameters, the three elision rules, structs that hold references, 'static, and why the compiler will not infer it for you.

Part III · Types that carry proofs (lessons 09–14)

Abstraction without giving up the guarantee: absence and failure as types, then traits, generics, trait objects and closures — each priced.

Enums, Option and match — absence and choice as types

There is no null and no moved-from state, so absence and choice must be types. Sum types, exhaustive match as a proof, Option and the niche that makes it free, patterns, and making illegal states unrepresentable.

Errors — Result, ?, and panic

Failure as a value the type system forces you to handle, forwarded with one character. From conversions, error enums, Box<dyn Error>; panic for bugs, unwinding runs Drop, and when each is right.

Traits — behavior as a checked contract

Name a behavior, promise it per type, and let the compiler check both sides. impl blocks, default methods, associated types, the coherence rule that keeps an impl globally unique, derive because there is no reflection, and receivers as ownership modes.

Generics and monomorphization — zero-cost polymorphism

Write it once, check it once at the definition, and let the compiler stamp out a copy per concrete type. Trait bounds, impl Trait, the cost table — speed, code size, compile time — and why this beats checking at instantiation.

Trait objects — dynamic dispatch as a priced choice

When the type is chosen at run time: dyn Trait is a fat pointer and a vtable. Dyn compatibility rules, Box<dyn Trait>, the price of an indirect call, and open sets (dyn) versus closed sets (enum).

Closures and iterators — abstraction that compiles away

A closure is a value that captures by shared borrow, exclusive borrow or move — the same three ownership modes. Fn, FnMut and FnOnce, unique closure types, lazy iterator adaptors that, in the build measured, compile to the loop you would write by hand, and iterator invalidation ruled out at compile time.

Part IV · When one owner is not enough (lessons 15–18)

The same law, checked later or across boundaries: shared ownership and interior mutability, threads, concurrent programs, and async tasks.

Smart pointers and interior mutability — the same law, checked later

Box for a heap owner, Rc and Arc for several, RefCell and Cell for mutation through a shared handle — the law checked at run time, by choice. Reference counts, cycles and Weak, the borrow flag, UnsafeCell as the one primitive, and Deref coercion.

Send and Sync — the law across threads

A data race is the law violated across threads. Two auto traits, derived structurally, say which values may cross or be shared between threads. Why Rc is not Send, what Arc and Mutex add, and how thread::spawn's bounds turn a race into a compile error — with a working trait solver.

Concurrent programs — channels, locks, scopes

Structure with the safe pieces: channels that move ownership, locks for sharing, scoped threads that borrow from their parent, atomics for the rest — and an honest list of what the promise still does not cover, deadlock first.

Async — futures as state machines

Thousands of waiting tasks without a thread each and without a runtime in the language. An async fn compiles to a state machine that stores the locals it needs across each await; Pin makes its self-references sound; the executor is a library. The price is a second dialect.

Part V · The trust boundary (lessons 19–20)

What the compiler cannot verify, a human must: unsafe, its obligations, and how to build a safe abstraction on it.

unsafe — taking the proof back

What the checker cannot verify, someone must. The extra powers, the obligations they create, what stays undefined, why unsafe does not switch the borrow checker off, soundness as the standard, and Miri as the sanitizer.

Building a safe abstraction on an unsafe core

From an unsafe core to an API no safe caller can break. split_at_mut and a minimal Vec built from raw parts: state the invariants, show each operation preserves them, and let privacy make the proof local.

Part VI · Shipping, and the honest bill (lessons 21–22)

Make the promises portable across teams, assemble everything, and price the bargain honestly.

Crates, Cargo, and privacy — promises that travel

Privacy as the soundness boundary, modules and crates, Cargo and semver, editions, and how a silent auto-trait change breaks a promise. Tests and doc tests that compile.

Capstone — a small concurrent service, and the honest costs

Assemble every mechanism into one program, walk the five questions over it, then price the bargain: the learning curve, the programs the checker refuses, compile times, async, the soundness holes still open. C++ trusts, Go constrains, Rust verifies — and where each belongs.

The whole derivation on one page

Read the second column of any row and the fourth column of the row above it: they are the same sentence. That is the linear thinking made visible — each lesson's problem it inherits is exactly the previous lesson's problem it creates, and the middle column is the single move that resolves the first and manufactures the second. The first row inherits its problem from the end of the C++ track; the last row hands its problem to you.

#	The problem it inherits	The one move	The problem it creates
Part I · The promise
00	The C++ track ended on a bargain: undefined behavior is the price of zero overhead, and the contract is kept by the programmer's promise alone. Could the compiler keep the contract instead, at the same zero cost?	Orientation: state the promise and the budget; the only place left for the proof is compile time	Suppose safe code must never exhibit undefined behavior, with no garbage collector and no run-time checking beyond the cheap ones. "Undefined behavior" is a long list of different bugs, and a compiler can only reject what it can recognize. What exactly must be ruled out, and what does each rule need to know?
01	Suppose safe code must never exhibit undefined behavior, with no garbage collector and no run-time checking beyond the cheap ones. "Undefined behavior" is a long list of different bugs, and a compiler can only reject what it can recognize. What exactly must be ruled out, and what does each rule need to know?	The promise, made precise: factor the seven bug families into cheap local fixes plus one law about names and places	Seven kinds of bug collapse into a handful of cheap local fixes plus one law: never mutate or free a place while another name can still reach it. To enforce that we need a precise vocabulary — place, value, name, lifetime — and a model of where values live. Where do values live, and what happens to them, in the simplest case?
02	Seven kinds of bug collapse into a handful of cheap local fixes plus one law: never mutate or free a place while another name can still reach it. To enforce that we need a precise vocabulary — place, value, name, lifetime — and a model of where values live. Where do values live, and what happens to them, in the simplest case?	Places, values, and the stack: fix the vocabulary; bounds, initialization and overflow become local rules	On the stack every value has a scope: it is created at its declaration and ends at the closing brace, automatically, exactly once. But a String, a Vec, anything whose size is decided at run time, lives on the heap, where nothing ends it automatically. Who frees it, and how do we make sure it happens exactly once?
Part II · Ownership and borrowing — the law
03	On the stack every value has a scope: it is created at its declaration and ends at the closing brace, automatically, exactly once. But a String, a Vec, anything whose size is decided at run time, lives on the heap, where nothing ends it automatically. Who frees it, and how do we make sure it happens exactly once?	Ownership — one owner, one drop: one owner per value; its scope end is the one drop	One owner, one drop: the language knows who frees each value. But assigning one owner to another copies its bytes, and a copied owner is a second owner of the same heap buffer — the double free is back. What must assignment mean for a value that owns something?
04	One owner, one drop: the language knows who frees each value. But assigning one owner to another copies its bytes, and a copied owner is a second owner of the same heap buffer — the double free is back. What must assignment mean for a value that owns something?	Move — assignment as transfer: assignment transfers ownership; the source is statically dead	Assignment moves ownership, which makes ownership safe but awkward: a function that only wants to read a value must take it and hand it back. How can code use a value it does not own, and stay safe while the owner is still alive and free to change it?
05	Assignment moves ownership, which makes ownership safe but awkward: a function that only wants to read a value must take it and hand it back. How can code use a value it does not own, and stay safe while the owner is still alive and free to change it?	Borrowing — the law: look without owning, under the law: shared readers or one exclusive writer	The law says many readers or one writer, never both — but it constrains borrows that overlap in time, and we have not said how long a borrow lasts. Nothing yet stops a reference from outliving the thing it points to. How long may a borrow live?
06	The law says many readers or one writer, never both — but it constrains borrows that overlap in time, and we have not said how long a borrow lasts. Nothing yet stops a reference from outliving the thing it points to. How long may a borrow live?	Lifetimes — a borrow is a region: a borrow is a region and must fit inside its owner's	A borrow's lifetime is a region of the program, and it must fit inside the owner's. So far we drew regions as nested blocks. The compiler has to compute them on real control flow — branches, early returns, reordered statements. What exactly does it compute?
07	A borrow's lifetime is a region of the program, and it must fit inside the owner's. So far we drew regions as nested blocks. The compiler has to compute them on real control flow — branches, early returns, reordered statements. What exactly does it compute?	The borrow checker — liveness: regions are liveness on the control-flow graph	The checker computes liveness inside one function body. A caller cannot read the callee's body, or checking would stop being modular and fast. When a function takes references and returns one, how does a caller learn which input the result borrows from, and for how long?
08	The checker computes liveness inside one function body. A caller cannot read the callee's body, or checking would stop being modular and fast. When a function takes references and returns one, how does a caller learn which input the result borrows from, and for how long?	Lifetimes in signatures — the modular contract: write the input-to-output borrow relationship down, so checking is modular	References are always valid and never null, and a moved-from name is dead, so there is nowhere to put no value here, or one of several shapes. How do we represent absence and choice without inventing null?
Part III · Types that carry proofs
09	References are always valid and never null, and a moved-from name is dead, so there is nowhere to put no value here, or one of several shapes. How do we represent absence and choice without inventing null?	Enums, Option and match: absence and choice become types, with an exhaustiveness proof	Absence and choice are types now, and failure is just one more choice carrying a payload. Checking and forwarding it by hand at every call is noisy, and some failures are bugs rather than events to handle. How should a program report, propagate and stop on errors?
10	Absence and choice are types now, and failure is just one more choice carrying a payload. Checking and forwarding it by hand at every call is noisy, and some failures are bugs rather than events to handle. How should a program report, propagate and stop on errors?	Errors — Result, ? and panic: failure is a value with a one-character propagation operator; bugs panic	We can model data precisely and handle failure — but every function so far works on one concrete type. How do we write code once for many types and still have the compiler verify that each type can do what the code needs?
11	We can model data precisely and handle failure — but every function so far works on one concrete type. How do we write code once for many types and still have the compiler verify that each type can do what the code needs?	Traits — behavior as a checked contract: behavior as a named, checked, globally-unique contract	A trait is a checked promise of behavior, but a promise is not machine code. To run generic code the compiler needs concrete types; unless every call is looked up at run time, which the budget rules out, that means generating a copy per type. What does that cost, and what does it buy?
12	A trait is a checked promise of behavior, but a promise is not machine code. To run generic code the compiler needs concrete types; unless every call is looked up at run time, which the budget rules out, that means generating a copy per type. What does that cost, and what does it buy?	Generics and monomorphization: one definition, checked once, erased at zero run-time cost	Generics fix each type at compile time: fast, but one concrete type per instantiation. When the type is chosen at run time — plugins, mixed collections, a list of different shapes — what is the alternative, and what is its price?
13	Generics fix each type at compile time: fast, but one concrete type per instantiation. When the type is chosen at run time — plugins, mixed collections, a list of different shapes — what is the alternative, and what is its price?	Trait objects — dynamic dispatch, priced: dynamic dispatch as an explicit, priced choice	Static and dynamic dispatch abstract over types. What about abstracting over behavior passed as a value — a piece of code together with the variables it uses? What can the variables it uses mean when every variable has an owner?
14	Static and dynamic dispatch abstract over types. What about abstracting over behavior passed as a value — a piece of code together with the variables it uses? What can the variables it uses mean when every variable has an owner?	Closures and iterators: the same three ownership modes, and abstraction that compiles away	Closures showed the three ownership modes at work: move, shared, exclusive. But everything so far has exactly one owner and a borrow law checked before the program runs. What about data that genuinely has several owners, or must change through a shared handle?
Part IV · When one owner is not enough
15	Closures showed the three ownership modes at work: move, shared, exclusive. But everything so far has exactly one owner and a borrow law checked before the program runs. What about data that genuinely has several owners, or must change through a shared handle?	Smart pointers and interior mutability: the same law, checked at run time, by choice	Rc and RefCell keep the law but check it while the program runs, within one thread. Threads share memory, and the same shared-mutation hazard between them is a data race. How does the law extend across threads?
16	Rc and RefCell keep the law but check it while the program runs, within one thread. Threads share memory, and the same shared-mutation hazard between them is a data race. How does the law extend across threads?	Send and Sync — the law across threads: the law across threads, derived structurally by the compiler	Send and Sync tell the compiler which values may cross, or be shared between, threads. Given those safe building blocks, how do we structure real concurrent programs — sharing, messaging, borrowing from a parent — and what does the promise still not cover?
17	Send and Sync tell the compiler which values may cross, or be shared between, threads. Given those safe building blocks, how do we structure real concurrent programs — sharing, messaging, borrowing from a parent — and what does the promise still not cover?	Concurrent programs: move over channels, lock to share, scope to borrow	Every thread costs a stack and a scheduler slot; ten thousand idle connections would need ten thousand threads. How can many tasks wait at once without a thread each, and without the language shipping a runtime?
18	Every thread costs a stack and a scheduler slot; ten thousand idle connections would need ten thousand threads. How can many tasks wait at once without a thread each, and without the language shipping a runtime?	Async — futures as state machines: a future is a compiler-generated state machine; Pin makes it sound	Since Rc and RefCell we have leaned on library types — Mutex, Vec, Pin — whose insides the checker cannot verify. What is inside them, what exactly is the compiler taking on trust, and who checks it?
Part V · The trust boundary
19	Since Rc and RefCell we have leaned on library types — Mutex, Vec, Pin — whose insides the checker cannot verify. What is inside them, what exactly is the compiler taking on trust, and who checks it?	unsafe — taking the proof back: extra powers, explicit obligations, and soundness as the standard	The keyword unsafe hands the proof to a human: the obligations are stated, but stating them is not discharging them. How do you build a safe abstraction on an unsafe core so that no safe caller, however hostile, can break it?
20	The keyword unsafe hands the proof to a human: the obligations are stated, but stating them is not discharging them. How do you build a safe abstraction on an unsafe core so that no safe caller, however hostile, can break it?	Building a safe abstraction: invariants plus privacy turn an unsafe core into a safe API	A sound abstraction survives only while its invariants stay private. How is code organized into modules and crates so that privacy is enforced, dependencies are managed, and other teams can rely on what you promise?
Part VI · Shipping, and the honest bill
21	A sound abstraction survives only while its invariants stay private. How is code organized into modules and crates so that privacy is enforced, dependencies are managed, and other teams can rely on what you promise?	Crates, Cargo, and privacy: make promises portable across teams	We now have every mechanism. What does the whole language look like assembled in one program, and what does the bargain honestly cost — where is it the wrong tool, and what should a careful engineer still weigh?
22	We now have every mechanism. What does the whole language look like assembled in one program, and what does the bargain honestly cost — where is it the wrong tool, and what should a careful engineer still weigh?	Capstone and the honest costs: assemble, price, and choose deliberately	Trust, constrain, verify: which belongs where in your own work, and what will you now ask of every line of code?

How to read this

Straight through, in order — the series is one argument, and each lesson's "Linear position" box names the problem it inherits, the single idea it adds, and the problem it hands on. If you only have time for the spine, read 00 → 01 → 03 → 05 → 07 → 16 → 19 → 22. To re-check the claims yourself on a newer compiler, run python3 tools/validate_rust_lessons.py --all from the repository root: it re-derives every badge, quoted error and widget from scratch.