The point of this work is to pin down the exact boundaries of undefined behavior. Certainly the code above is
accepted by the Rust compiler, but it also
breaks rules. What rules? In essence, we know that:
- Anything accepted by the borrow checker is legal
- Unsafe can express illegal / undefined behavior
- There's some set of rules, broader than what the borrow checker can check, that is still legal / defined behavior
The goal of this line of work is to precisely specify that set of rules. The outlines are clear (basically, no writable pointers should alias) but the details (interior pointers, invalidation of iterators, is it creating or using bad pointers that's bad, etc) are really hard. The previous paper in this series, on Stacked Borrows, was simpler but more restrictive, and real-world unsafe code often failed its rules (while still seeming correct). Tree Borrows is broader and allows more while still being provably safe.