The correctness of a given program may be global, if it's putting pointers everywhere. So while correctness of the program over all inputs may require global reasoning in the general case, the Stacked Borrows model is still extremely localizable. In fact, this is exactly what safe references do: they take (whatever formal aliasing model the Rust Abstract Machine requires) and, by the use of lifetimes, restrict it to a locally-machine-checkable subset.
The Stacked Borrows model is essentially taking raw pointers and assigning them the exact same lifetime rules as references have. The only difference is that the lifetime extent of the raw pointers (point-of-creation to point-of-last-use) is under your control, not bound to some (non)lexical scope. Importantly, this directly implies one of the rules you take issue to:
- Deriving a pointer from
&mut, then using that
&mutagain (for any purpose) invalidates the derived pointer.
This is exactly the same rules enforced by the borrow checker. Maybe it helps to turn the condition on its head: rather than "using this reference invalidates all pointers derived from it" (less local), it's "while derived pointers are still alive (may be used in the future), it's illegal to use this reference" (more local).
So you localize pointer provenance reasoning the exact same way you do with references: you document what the lifetimes are. The lifetimes are obviously more complicated with pointers (otherwise you'd just use references), but they still exist, and you need to document and follow them to make reasoning about correctness tenable.
I find Stacked Borrows surprisingly simple to reason about. Perhaps I'm just overconfident. But at the same time, I think it's very similar to learning to work with lifetimes for the first time: it can seem overly restrictive at first, but as you learn to structure your logic in the way the system wants you to, it gets easier to work with and reason about.
Stacked Borrows isn't perfect as is. Specifically, I'd like to see a proposed solution to the "
&Header issue," because that's a large footgun I don't think is strictly required to build a consistent and useful model. But I don't find it as problematic as you're making it out to be.
I don't think the answer is a significantly weaker aliasing model. Rather, I think the solution is more best-effort lints for patterns like
let a = &mut x as *mut _; let b = &mut x as *mut _; *a; that are statically detectable, that give the better way to do it that doesn't run afoul of the aliasing model (
let a = &raw mut x; let b = &raw mut x; *a;). It's in providing more tools to write code that happens to be
unsafe without shaming the developer with too much syntactic salt.