Lecture, Conference Presentation
Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming
Jane StreetDerek Dreyer, Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Hoang-Hai Dang, Jan-Oliver Kaiser
- The "Rust Belt" project aims to apply logical foundations developed over the past decade to the Rust programming language to verify safety guarantees for the core type system and widely used libraries.
- Future development plans include evolving the language safely and creating more automated verification technology to systematically prove API safety.
- The "Iris" framework is expected to serve as a unified foundation for deriving new separation logics, encoding semantic models of Rust types, and enabling the derivation of reasoning principles like the "borrow proposition" without bespoke logics.
- The initiative plans to demonstrate the specification and verification of the
Arc(Atomic Reference Counting) API and the encoding of work on relaxed memory models and concurrent separation logic within the Iris framework. - Current semantic models rely on a simplistic "CompCert-like" memory model, with ongoing work to define a future model that incorporates more undefined behavior to support compiler optimizations.
- While the Iris framework is designed to allow adaptation of the semantic model for adventurous APIs and replace complicated primitive rules with user-defined logical state, a fully realistic memory model that balances developer expectations with safe LLVM compilation remains an open question.
- The project seeks to address the trend where new libraries require new separation logics by utilizing partial commutative monoids to provide a generic algebraic structure for representing logical state.