This thesis provides a mathematical formalization of Polonius, the next-generation borrow checker for the Rust programming language. Rust's distinguishing feature is its ability to guarantee memory safety through its type system and borrow checker, ensuring safety without impacting runtime performance. The current implementation, known as NLL (Non-Lexical Lifetimes), remains overly conservative in certain cases -- consequently, Rust developers have introduced a new version called Polonius, which is based on a more precise data-flow analysis. However, Polonius lacks an official specification, and information regarding its workings remains scattered. The goal of this thesis is to establish a mathematical framework that enables a clear understanding of this new implementation. This is approached using sets and logical statements, describing the rules established in various sources through predicates and inference rules. The final result is a simplified but formal description of Polonius.
|
