Oxide: The Essence of Rust.
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. We present Oxide, a
formalized programming language close to source-level Rust (but with
fully-annotated types). This presentation takes a new view of lifetimes as an
approximation of the provenances of references, and our type system is able to
automatically compute this information through a substructural typing judgment.
We provide the first syntactic proof of type safety for borrow checking using
progress and preservation. Oxide is a simpler formulation of borrow checking -
including recent features such as non-lexical lifetimes - that we hope
researchers will be able to use as the basis for work on Rust.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.