Rust aims to archive the holy grail of a language that gives low-control over resource management and safe high-level abstractions. It does this using a type system that restricts programs to eliminate unsafe programming practices coupled with a practice of extending that type system with libraries that are observably safe but that internally use “unsafe” operations. This paper provides a framework for proving that these libraries do not break the safety guarantees of the standard type system. Along the way, the paper gives a nice insight into the way that the community as a whole has been developing.
This paper departs from standard practice over the last 20 or so years of using syntactic techniques to prove results about the type system. They argue that these syntactic techniques are closed-world methods but Rust’s extensible type system requires an open-world approach. So they revert to the older practice of proving type soundness semantically. This is done in the Iris framework building on “step-indexed” logical relations for scalability.
After a tour of the key concepts in Rust’s ownership type system, they present lambda-rust which is at a level simile are to Rust’s Mid-level Intermediate Representations (MIR) and is (roughly) a continuation passing lambda calculus extended with lifetimes.
For a more detailed summary, I recommend the morning paper.
Notes related to RustBelt: Securing the foundations of the Rust programming language
Papers related to RustBelt: Securing the foundations of the Rust programming language
- Engineering the Servo web browser engine using Rust [anderson:icse:2016]
- Safe systems programming in Rust: The promise and the challenge [jung:cacm:2021]
- Stacked borrows: An aliasing model for Rust [jung:popl:2020]
- Crust: A bounded verifier for Rust [toman:ase:2015]
- GhostCell: Separating permissions from data in Rust [yanovski:unknown:2021]