Often, it's a matter of excess being as bad as deficiency.
Tree Borrows is a new specification proposed by the Programming Language Foundations Laboratory at ETH Zurich, aiming to precisely define the boundaries of unsafe blocks in Rust that may lead to undefined behavior (Undefined Behavior, UB). Rust employs the ownership concept in its type system, offering strong guarantees for memory safety and avoiding data races. However, its unsafe blocks provide certain exceptions that must be manually maintained by programmers for safety. To prevent misuse of unsafe code while preserving the performance of powerful compiler optimizations (such as pointer aliasing optimizations), the traditional Stacked Borrows model has attempted to establish related rules but often proves too strict and inconsistent with common practical patterns. Tree Borrows replaces the stack with a tree structure, addressing the original limitations and supporting more grammar patterns.
According to the research team's experiments, Tree Borrows reduced the number of rejected cases for improper usage by 54% when analyzing 30,000 widely used Rust packages, demonstrating its higher tolerance for real-world programming needs. Additionally, the paper used the Rocq tool to prove that the new specification not only retains most existing optimization strategies but also introduces novel optimizations such as read-after-write reordering, further enhancing the safety and performance of the compilation process.
In the discussion forum, some netizens mentioned that the early Stacked Borrows model had attracted attention in 2018 and 2020, mainly due to its overly narrow definition of unsafe code behavior. Several discussants emphasized that although the Rust compiler may accept certain code, these codes actually violate the strict rule of non-coexisting mutable references, leading to undefined behavior. Another netizen cited Ralf Jung's blog, adding that Tree Borrows not only helps eliminate these counterexamples but also provides a theoretical foundation for more precise descriptions of Rust's operational semantics in the future.
This study, which won the PLDI'25 Distinguished Paper Award for its in-depth analysis and innovative solutions to the boundary issues of unsafe code, is considered an important achievement in advancing the safety and optimization theory of the Rust language. The discussion also humorously noted that the author Neven Villani is the son of renowned mathematician Cédric Villani, highlighting the widespread attention this research has received in both academic and practical circles.
https://news.ycombinator.com/item?id=44510600