Borrow checking in Rust is usually described as a feature of the type system. Lifetimes appear in type signatures, the borrow checker runs over typed intermediate representations, and the whole apparatus is presented as inseparable from Rust’s ownership types. This framing is understandable but misleading. The core insight in a recent piece on scattered-thoughts.net is that the safety analysis itself does not require type information. You can check ownership discipline on a program without knowing anything about what types its values carry.
This distinction matters more than it might seem.
What Borrow Checking Actually Does
Strip away the surface syntax of Rust and what the borrow checker actually does is track variable states through control flow. For each point in a program, it maintains information about every variable: is it initialized, is it moved, is it borrowed, and if borrowed, is that borrow shared or exclusive? When two code paths merge, it reconciles the states from each branch. When you pass a value to a function, it marks it as moved. When you take a reference, it tracks when that reference expires.
None of this analysis requires knowing whether a value is a Vec<u32> or a custom struct. The analysis runs on variable names and control flow paths. The type information that does appear in Rust’s borrow checker mostly exists to resolve lifetimes on function signatures, to handle generics, and to enforce that types implement Send and Sync correctly. These are real requirements, but they are requirements for the type system, not for the ownership analysis itself.
The ownership analysis is a form of dataflow analysis, specifically an instance of what the PL literature calls liveness analysis combined with alias tracking. Both of these techniques predate Rust by decades and neither requires a type system to operate.
How Rust Entangled the Two
Rust’s design wove ownership into the type system deliberately. Lifetimes became parameters on types. References became types in their own right: &'a T and &'a mut T carry their aliasing properties in the type signature. This was a reasonable design choice because it makes ownership constraints checkable at module and crate boundaries, where the compiler only has type information available.
If you want to write a library function that accepts a reference and returns a reference derived from it, you need to communicate the lifetime relationship in the type signature. The borrow checker then enforces that callers satisfy those constraints. This is where types and ownership genuinely intersect: at API boundaries, ownership constraints need to be expressible in the type system so they survive compilation unit boundaries.
Inside a single function or a closed piece of code, though, the ownership constraints are entirely determined by the control flow structure. No type information is needed.
Rust’s Polonius project has been moving in a direction that makes this separation more explicit. Polonius reformulates borrow checking as a Datalog computation over facts, where the facts describe control flow, variable definitions, uses, and borrows. Type information feeds in as additional facts, but the analysis engine itself operates on a graph of variable states and flow edges. This architectural separation reflects the underlying reality: ownership is a property of programs, not of types.
Prior Art in the Separation
Language designers have explored ownership and types as separate concerns several times.
The Cyclone language, developed at Cornell in the early 2000s as a safe variant of C, used region annotations to track memory lifetimes. These regions were partly integrated into the type system but the region analysis itself operated on control flow. Cyclone’s goal was to add safety to an existing unsafe language, which required treating the ownership analysis as somewhat detached from the base C type system.
The Clean language uses uniqueness types, which are orthogonal to the value types. A value can have type *Int (unique integer) or Int (non-unique), and the uniqueness annotation is tracked separately from the type hierarchy. The uniqueness analysis enforces single-use properties without merging the ownership semantics into the main type lattice.
Pony takes this further with reference capabilities, which are annotations on references that specify sharing and mutability properties. A String iso and a String val have the same underlying type String but different reference capabilities. The capability analysis, which enforces data-race freedom, operates largely independently from type-checking the String value itself.
All of these designs arrive at a similar conclusion: ownership is a capability or a property of references, not of values, and tracking it separately from value types is both possible and workable.
What the Separation Enables
The practical value of separating these concerns becomes clear when you ask what languages borrow checking might be useful in beyond languages designed with ownership from the start.
Python has a garbage collector, but it also has a persistent problem with mutable shared state in concurrent code. The Global Interpreter Lock exists partly because tracking aliasing in Python is genuinely hard. An ownership analysis on Python bytecode or AST could identify locations where mutable values escape into shared state, without requiring any changes to Python’s type system. Tools like Pyright and mypy demonstrate that layered static analyses on Python code are practically useful even when the language does not enforce them at runtime.
The same argument applies to Lua, JavaScript, and other scripting languages. Borrow checking as a linter, operating on control flow without integrating into the type system, would catch a class of bugs that type checkers do not address.
For new language design, the separation is useful in a different way. A compiler implementer can run ownership analysis in an early pass, before type inference has completed, and surface ownership errors while the program’s structure is still clear. Rust’s borrow checker runs after type checking, which means borrow errors can be obscured by type errors or presented in terms of inferred types that the programmer did not write. An earlier ownership pass might produce cleaner diagnostics.
There is also a connection to gradual typing. A language that wants to introduce ownership safety incrementally could add an ownership analysis layer without requiring the full apparatus of lifetime-parameterized types. Modules that opt into ownership checking get the analysis; modules that do not are treated as opaque from the ownership perspective.
The Limits of the Separation
Separating ownership from types does not eliminate all the hard problems.
Function calls remain the difficult case. When a function accepts a value, the caller needs to know whether the function consumes it, borrows it, or borrows it mutably. Without type signatures that carry ownership information, you need either inference (the analysis infers how each call site behaves based on the function body) or annotations (the programmer marks functions with ownership contracts). Inference does not scale across compilation units; annotations are a form of ownership type system even if they are not integrated with the value type system.
Generics compound the problem. A generic function that works over arbitrary types needs to express ownership constraints that apply regardless of what type fills in the type parameter. This is precisely where Rust’s lifetime parameters on types earn their complexity.
So the claim is not that you can build a full ownership-safe language without any type-level ownership concepts. The claim is that the core analysis, the dataflow tracking of borrows and moves, can run independently of type information, and that confining type-level ownership concepts to function signatures and API boundaries is a coherent and workable design.
Why This Is Worth Thinking About
Rust made ownership mainstream, but it bundled the safety analysis together with a specific type-system design that has significant learning-curve costs. Lifetimes in type signatures are one of the primary barriers for developers coming to Rust from other languages. Separating the ownership analysis from the type system is one path toward making memory safety analysis available in contexts where the full Rust type system is either too expensive to adopt or simply unavailable.
The work described in the scattered-thoughts.net article explores whether that path is coherent, and the early evidence is that it is. Borrow checking is dataflow analysis. Dataflow analysis does not require types. The coupling we have inherited from Rust’s design is partly a consequence of historical choices about where to draw architectural boundaries in a compiler, not a fundamental requirement of the safety guarantee.
That realization opens up a genuinely interesting design space for language tooling and compiler architecture, and it is the kind of fundamental observation that tends to produce useful new tools in the years after someone takes the time to write it down carefully.