Derek Dreyer
Showing 1–1 of 1 transcripts.
- Jane Street1h 6m
Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming
Derek Dreyer, Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Hoang-Hai Dang, Jan-Oliver Kaiser
The MPI for Software Systems' "Rust Belt" project applies decades of academic research to formally verify the safety guarantees of the Rust programming language against the risks posed by "unsafe" code. By leveraging the Iris framework and mechanizing proofs in the Coq assistant, the team establishes a semantic safety model that independently verifies complex libraries like `Arc` and `Mutex`, successfully identifying critical bugs in memory ordering and reference counting. This methodology ensures that future language evolution and standard library modifications can proceed with mathematical certainty that undefined behavior remains impossible.