Abstract
Continuing the theme of scaling mechanized semantics, the sixth seminar described recent work on formalizing the Rust language. After recalling the basic concepts of the Rust type system, in particular the temporary possession and borrowing of mutable data structures, the speaker described their formalization in the λ-rust system. Types are semantically interpreted as separation logic formulas, demonstrating the safety of typing even in the presence of non-typable " unsafe " code, provided the latter is verifiable in separation logic. This work leads to a suggestion for improving the semantics of Rust : a pointer sharing model called stacked borrows, which enables further optimizations at compile time.
