Ownership Tracking as Program Analysis: What Decoupling the Borrow Checker Actually Requires

Jamie Brandon’s recent post on borrow-checking without type-checking asks a question that sounds almost heretical if you’ve spent any time with Rust: can you have the safety guarantees that a borrow checker provides without building a full static type system to carry them? The question is worth taking seriously, because the coupling between Rust’s ownership model and its type system is so deep that most people treat them as inseparable. They are not.

What the Borrow Checker Actually Does

Rust’s borrow checker operates on MIR, the Mid-level Intermediate Representation that sits between the typed AST and code generation. By the time the borrow checker runs, type inference is complete and every variable has a known type, including lifetime parameters. The checker then performs a form of liveness analysis: it builds a constraint system over lifetime variables, propagates them through the control flow graph, and checks that no mutable borrow aliases with any other borrow of the same place, and that no reference outlives the data it points to.

The key insight is that most of this analysis is fundamentally about data flow, not types. The borrow checker is asking: at any given program point, which variables alias which memory locations, and what access rights do those variables have? That is a question that can, in principle, be answered through program analysis without a fully specified type system. The complication is function call boundaries.

The Compositionality Wall

Within a single function body, tracking ownership is straightforward. Consider a simple Rust example:

fn example() {
    let mut v = vec![1, 2, 3];
    let r = &v[0];
    v.push(4); // error: cannot borrow `v` as mutable because it is also borrowed as immutable
    println!("{}", r);
}

The error here requires no knowledge of types beyond “v is a thing and r borrows part of it.” A flow analysis over the control flow graph can determine that r is live at the push call site and that push takes a mutable reference to v. You don’t need a fully elaborated type signature to detect this conflict within a function body.

Function calls are where this breaks down. When you write:

fn process(data: &mut Vec<i32>, index: &i32) { ... }

Rust’s type system encodes the information that data and index must not alias, that the function borrows its first argument mutably and its second immutably, and that both borrows end when the function returns. This information is part of the function’s type signature. A caller can check its own borrow constraints by reading that signature without looking inside the function body.

Without that type-level information, checking becomes a whole-program problem. To verify that a call to process is safe, you’d need to inline the analysis of process at every call site, or run an interprocedural alias analysis that propagates ownership information across call boundaries. Both approaches exist in the program analysis literature; neither scales as well as Rust’s modular, signature-based approach.

Prior Art: What Languages Have Tried

Several languages and tools have explored different points on this spectrum.

Cyclone, a safe dialect of C developed at AT&T Research, added region and lifetime annotations directly to C’s type system. It was essentially a demonstration that you could retrofit ownership tracking onto an existing language, but it required adding type-level machinery to carry the ownership information. The annotations were the price of modularity.

Facebook’s Infer takes the opposite approach. It uses bi-abduction and separation logic to find memory bugs in C, Java, and Objective-C programs without requiring any ownership annotations from the programmer. It works through interprocedural analysis: it infers pre- and postconditions for functions in terms of heap shapes, then verifies call sites against those inferred contracts. This works remarkably well in practice and has found thousands of bugs in production codebases. The trade-off is that it is a bug-finding tool, not a proof of safety. It can miss bugs when the interprocedural analysis doesn’t converge on the right invariant.

The Lobster language by Wouter van Oortmerssen uses what the author calls compile-time reference counting (CTRC). The compiler performs escape analysis to determine which allocations can be stack-allocated, which can be reference-counted without cycles, and which require full GC. This is not borrow checking in the Rust sense, but it is ownership tracking through program analysis rather than through a fully specified ownership type system. The result is a language that has no explicit lifetime or ownership annotations but still achieves substantial automatic memory management with low overhead.

Pony encodes aliasing permissions in its type system through reference capabilities: iso, trn, ref, val, box, and tag. These are type-level, but the capability system serves a different primary goal than Rust’s lifetimes. Pony’s capabilities are primarily about data race freedom in a concurrent actor model, and they’re checked at the type level because the language needs to be able to verify safety at function call boundaries without whole-program analysis. The types carry the ownership information.

Separation Logic and What It Tells Us

Separation logic, introduced by John Reynolds and Peter O’Hearn in the early 2000s, provides a mathematical framework for reasoning about heap aliasing. The separating conjunction P * Q asserts that P and Q hold on disjoint parts of the heap. This is exactly the kind of aliasing information a borrow checker needs to verify.

Tools like RefinedC, Verifast, and Iris use separation logic to verify C and Rust programs. What’s notable is that the most effective versions of these tools still require function contracts: pre- and postconditions expressed in separation logic terms. The contracts serve the same compositionality function that type signatures serve in Rust. You can do without them, but only by accepting whole-program reasoning.

This keeps pointing to the same structural constraint: modularity requires that function boundaries carry some ownership information, whether that information is encoded in types, in contracts, or in some lighter-weight annotation form.

What “Without Type-Checking” Can Mean in Practice

There are a few genuinely different things the phrase could mean, and the answer changes depending on which one you have in mind.

The first is decoupling borrow checking from type inference. Rust’s borrow checker runs after type inference is complete. In principle, you could design a language where ownership is tracked by a separate analysis phase that operates on untyped or partially-typed terms, using type information only where it’s available. This is closest to what some gradual typing research explores.

The second is borrow checking in a dynamically typed language. This is the hardest version of the problem. Without static types, you don’t know at compile time what type a variable holds, so you can’t know statically whether two variables might alias the same data through an interface boundary. You’d need to either restrict the analysis to patterns you can prove statically (a conservative overapproximation that produces false positives) or insert runtime checks for aliasing constraints.

The third, and most tractable, is borrow checking with a simpler or implicit type system. A language where types are inferred entirely, lifetimes are inferred rather than annotated, and function signatures are computed rather than declared could still run a borrow checker. This is essentially what Rust was moving toward with NLL (Non-Lexical Lifetimes) and the polonius project. Polonius, the next-generation Rust borrow checker, reformulates lifetime inference as a Datalog program. The lifetimes are still computed, just through a different mechanism than the current constraint solver.

The Trade-Off Is Always Compositionality vs. Annotation Burden

The deeper pattern here is not specific to borrow checking. Any static analysis that wants to be modular needs some kind of summary at module boundaries. Types are one way to express those summaries; effect systems are another; contracts and pre/postconditions are a third. The choice of mechanism determines what you can express, how much the programmer must write, and how the analysis scales.

Rust’s lifetime annotations are verbose. The lifetime elision rules hide most of them in practice, but they’re still there conceptually, and they surface whenever you write a function that returns a reference or stores one in a struct. That annotation burden is the price Rust pays for modular, local borrow checking that doesn’t require whole-program analysis.

A language that removes those annotations either pays the cost of whole-program analysis, accepts weaker safety guarantees, or discovers that some lighter-weight form of annotation (capability markers, effect labels, region names) is unavoidable. The borrow checker can be separated from type checking in various ways, but something must carry the ownership information across function call boundaries, and whatever carries it will look, to some degree, like a type system for ownership.

Brandon’s exploration is valuable precisely because it probes these limits carefully. The question of whether the safety guarantees can be preserved with a lighter annotation burden than Rust requires, or through a different analysis architecture, is one the language design community has been circling for years. The honest answer is: sometimes yes, always with a trade-off, and the trade-off always lives at the same structural point.