You have now lost about twenty arguments with the borrow checker. That is the prerequisite for this article; delivered any earlier it would be a slogan.
Most people arrive at Rust with a model in which the compiler is a fussy style checker to be placated. Under that model every error feels arbitrary, every fix feels like a hack, and the correct response to a rejection is to shuffle code until the complaining stops. It is a coherent model. It is also wrong, and it makes the language much harder than it is.
The replacement is one sentence: the borrow checker is a proof system, and a rejection means you have not handed it a proof.
That is not a metaphor and not a motivational framing. It is literally what the component does. Four claims, each defended.
Claim 1: it is an analysis, not a heuristic
The borrow checker does not pattern-match on your source code. It runs after type checking, on MIR — rustc’s mid-level intermediate representation, a control-flow graph of basic blocks with explicit StorageLive/StorageDead markers and explicit borrow, move and drop operations.
Over that graph it performs region inference. Every reference in the program gets a region variable; every use of a reference generates a constraint that the region must include that program point; every subtyping relation generates an outlives-constraint between regions. The solver propagates those constraints backwards through the CFG to a fixed point, producing for each loan the exact set of program points where it is live. Then it checks, at each point, that no two live loans conflict under the shared-XOR-exclusive rule.
This is why the behaviour you have observed is what it is:
- A borrow ends at its last use (item 3.5), because liveness is computed from uses, not from lexical scopes.
-
if false { ... }still counts (item 3.3), because the branch is a node in the CFG regardless of whether it executes. - The analysis stops dead at function boundaries (item 3.15), because it consumes signatures and never bodies.
-
It is not interprocedural about aliasing (item 3.19), because
&mutin a signature is the interprocedural fact, asserted rather than inferred.
Every one of those follows from “control-flow-sensitive region inference over MIR”. None of them follows from “a linter with opinions”.
💡If the checker never reads the body of a function you call, how can split_at_mut possibly be sound? Something must have checked it.
click to reveal
Something did — once, at the definition, by a human, with unsafe.
split_at_mut is implemented with raw pointers and an unsafe block, and its body carries a // SAFETY: comment arguing that mid <= len partitions the buffer into two non-overlapping ranges. The compiler did not verify that argument. A person wrote it, other people reviewed it, and Miri exercises it.
What the compiler does verify is that every caller respects the signature: one &mut [T] in, two &mut [T] out with the same lifetime. Callers get the disjointness guarantee for free and forever, and the obligation was discharged exactly once.
This is the whole architecture of safe Rust. A small, audited, unsafe core proves things the checker cannot; the vast safe surface above it consumes those proofs through types. Vec, Rc, Mutex, iter_mut, split_at_mut are all this shape. When you meet a wall, the productive question is not “how do I get around the checker” but “who has already proved this and what did they call it”.
Claim 2: it aims at soundness, not completeness
A static analysis of a Turing-complete language cannot be both sound (never accepts a bad program) and complete (never rejects a good one). You choose. The borrow checker chooses soundness, without apology.
So the set of programs it accepts is a strict subset of the programs that are actually fine. Some correct programs are rejected. That is not a defect to be fixed in a future release; it is a permanent, deliberate property of the design.
The practical consequence is a change of question. When your program is rejected, the useful question is not “is my program correct?” — it very often is. The useful question is “can I hand the compiler a proof it is able to check?”
Once you ask that, the moves you have learned in this track stop looking like a bag of tricks and start looking like a catalogue of proof-carrying constructs:
-
split_at_mut,get_disjoint_mut,chunks_mut— proofs of disjointness. -
iter_mut— a proof that references are handed out one at a time and never revisited. -
entry— a proof that lookup and insertion are a single borrow. -
mem::take,mem::replace— proofs that a move out is immediately compensated. -
thread::scope— a proof that spawned threads end before the borrowed data does. -
Destructuring
self— turning one place the signature cannot subdivide into several the checker can.
“The compiler is wrong” is almost always “the compiler cannot prove it”. There is exactly one shape in modern Rust where the stronger claim is fair, and it has a name and a number: NLL Problem Case #3 (item 3.20), acknowledged since 2017, with a fix (Polonius) that is a nightly prototype and a 2026 project goal rather than a shipped feature.
Claim 3: therefore every rejection is exactly one of three things
This is the practical payload of the article. When the borrow checker rejects your code, it is one of:
(1) Your program is genuinely wrong. There really is a use-after-free, an iterator invalidation, a double-free, a data race. This happens more often than wounded pride suggests. Before doing anything else, ask what would go wrong at runtime if the compiler let this through — item 3.6’s starter has a real use-after-free in it, and item 3.12’s has the bug that C++ leaves as undefined behaviour and Python silently gets wrong.
(2) Your program is right, but you have not handed over a consumable proof. By far the most common case. The fix is to restructure — copy the value out, shorten the loan, compute-then-mutate — or to reach for a standard-library construct that carries the proof. The catalogue above is your first stop.
(3) The analysis is genuinely too weak. Today this means NLL Problem Case #3, and essentially nothing else. If you think you are in category (3), you are in category (2) roughly ninety-nine times out of a hundred.
Learning to triage quickly between those three is the skill. It is what separates “I fought the borrow checker for an hour” from “oh, that’s a (2), I need entry“.
💡Go back through this track and pick three problems where your first attempt was rejected. Classify each as (1), (2) or (3). What did the (1)s have in common? click to reveal
A likely honest answer, and worth checking against your own history:
Category (1) — genuinely wrong. Item 3.12’s compact starter, mutating a vector while iterating it, is a real use-after-free in any language without the rule. Item 3.6’s append_first, holding a &i64 into a buffer across a push that may reallocate, is the same bug in miniature. What they have in common: in both, the reference points into a container whose storage the mutation can move. That is the shape to learn to recognise — a borrow of an element, held across an operation that can reallocate.
Category (2) — right, but unproven. Item 3.7’s two &mut xs[i] (the compiler cannot do arithmetic across an IndexMut call), item 3.15’s self.note() while scanning self.items (the signature cannot say “only these fields”), item 3.16’s fold across halves. All three are correct programs, and all three are fixed by naming a construct that already contains the proof.
Category (3) — genuinely too weak. Item 3.20’s bump, and only that.
If your (1) list is empty, look again. Everyone has at least one, and finding it is the moment the checker stops feeling adversarial.
Claim 4: unsafe is the proof obligation changing hands
unsafe does not turn checks off. Type checking, borrow checking, and lifetimes all still run inside an unsafe block exactly as they do outside it. What unsafe unlocks is a short list of extra abilities — dereferencing a raw pointer, calling an unsafe fn, implementing an unsafe trait, reading a union field, accessing a mutable static.
What actually happens at the unsafe keyword is a transfer of responsibility. Up to that point, the compiler was carrying the obligation to prove memory safety. Inside, you are. The invariants are the same; the prover changed.
That reframing explains a convention that otherwise looks like bureaucracy. A // SAFETY: comment above an unsafe block is not politeness and not documentation-for-its-own-sake. It is the proof, written in the only notation available. It is the artefact the compiler would have produced if it could, and it is what a reviewer checks. A missing // SAFETY: comment is a missing proof, which is why clippy::undocumented_unsafe_blocks exists and why serious codebases deny it.
Rust 2024 sharpens the same point: unsafe_op_in_unsafe_fn is now the default, so marking a function unsafe no longer makes its whole body an implicit unsafe block. Declaring “callers must uphold X” and performing unchecked operations are two separate acts, and the edition makes you write both.
The contrast that gives this article its title
Clippy is a linter, and comparing the two makes the distinction concrete.
| borrow checker | clippy | |
|---|---|---|
| false positives | rejects some correct programs, by a soundness argument | has genuine false positives, filed as bugs |
| suppression |
none — no #[allow], no flag, no opt-out in safe code |
#[allow(clippy::...)] is normal and often correct |
| disagreement | not a matter of opinion |
reasonable people disagree with pedantic and style daily |
| authority | a property of the language | a collection of opinions, revisable per release |
You met that difference concretely in item 3.13: clippy’s needless_range_loop sometimes suggests code that does not compile, and #[allow(clippy::needless_range_loop)] with a one-line justification is a legitimate professional outcome. There is no equivalent move for E0499. You do not get to allow it, argue with it, or explain that you were careful. You hand over a proof or you restructure.
Both tools are worth having. They are not the same kind of thing, and treating the checker like a linter is the mistake that makes Rust feel arbitrary.
One thing not to claim
Rust’s safety guarantees have not been machine-checked for real rustc, and you should not say they have.
What exists is RustBelt (Jung, Jourdan, Krebbers, Dreyer) — a machine-checked proof in Coq, using the Iris separation-logic framework, that a realistic subset of Rust called λRust is sound, and a method for proving that specific unsafe library abstractions (Cell, RefCell, Rc, Arc, Mutex, RwLock, thread::scope) uphold their interfaces. That is a genuine and important result. It is also a proof about a formal model, not about the compiler in your ~/.cargo.
Real rustc has had soundness bugs and has fixed them. The #[may_dangle] / dropck story, several variance and lifetime-inference holes, and a number of trait-solver issues are all documented in the issue tracker with the I-unsound label. The number is small and shrinking, and every one has been treated as a release-blocking emergency — which is the actual evidence of the project’s seriousness, more than any proof would be.
So: the borrow checker is a proof system whose design has been shown sound for a realistic core, implemented by humans who occasionally get it wrong and fix it fast. That is a stronger and more honest claim than “Rust is proven safe”, and it is the one to carry out of this track.
Where this leaves you
You have the axiom (item 3.3), the reading procedure for a diagnostic (item 3.4), the liveness rule (item 3.5), a triage checklist (item 3.6), the catalogue of proof-carrying APIs (items 3.7, 3.14, 3.16, 3.20), the two pieces of invisible machinery (items 3.17, 3.18), the honest limit (item 3.20), the runtime escape hatch and its price (item 3.22), and the reason the rule is not negotiable (item 3.23).
The rest of Rust is easier than this track. Ownership and borrowing are the part that has no analogue in the languages you already know; everything after it — traits, generics, error handling, iterators, concurrency — is a thing you have seen before, done more carefully.
When the next rejection arrives, ask the three-way question. Which of (1), (2), (3) is this? You will almost always be able to answer within a minute, and the answer will tell you what to do.