The Rust programming language is well known for its ownership-based
type system, which offers strong guarantees like memory safety and data race freedom.
However, Rust also provides unsafe escape hatches, for which safety is not guaranteed
automatically and must instead be manually upheld by the programmer.
This creates a tension. On the one hand, compilers would like to exploit the strong
guarantees of the type system in order to unlock powerful intraprocedural optimizations.
On the other hand, those optimizations are easily invalidated by “badly behaved” unsafe code.
To ensure correctness of such optimizations, it thus becomes necessary to clearly define what
unsafe code is “badly behaved”.
We present Tree Borrows, a set of rules improving on prior work to achieve this goal.