Oxide: The Essence of Rust

Understand

Rust claims to advance industrial programming by bridging the gap between low-level systems programming and high-level application programming.

• At the heart of the argument that this enables programmers to build more reliable and efficient software is the borrow checker - a novel approach to ownership that aims to balance type system expressivity with usability.
• And yet, to date there is no core type system that captures Rust's notion of ownership and borrowing, and hence no foundation for research on Rust to build upon.
• In this work, we set out to capture the essence of this model of ownership by developing a type systems account of Rust's borrow checker.