RustBelt: A Quick Dive Into the Abyss - Formalizing Rust's Safety Story

Dive into the depths of Rust's safety mechanisms with this 30-minute conference talk by Ralf Jung and Michael Sammler. Explore the RustBelt project, which aims to formalize Rust's safety story. Gain insights into the Arust type system and understand the concept of syntactic type safety. Learn about the semantic interpretation of types and how it lifts to all judgments. Discover how unsafe code is composed within the Rust ecosystem. Delve into the intricacies of lifetime logic and semantic well-typedness, with a focus on Cell::new and its sharing predicates. Examine the semantic well-typedness of Cell::set and witness practical implementations of Cell::new and Cell::replace in Coq. Enhance your understanding of Rust's underlying safety principles and formal verification techniques.

Intro
RustBelt - formalizing Rust's safety story
The Arust type system
Syntactic type safety
1. Semantic interpretation of types
2. Lift to all judgments
Composition with unsafe code
Lifetime logic
Semantic well-typedness of Cell::new: E
Sharing predicates
Semantic well-typedness of Cell::set: E
Cell:new in Coq
Cell:replace in Coq