RustBelt: Logical Foundations for the Future of Safe Systems Programming

Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff in language design between high-level safety guarantees and low-level control over resource management.  Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold.  Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features.  In this work, we present RustBelt, the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language.  We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

In the talk, I will review some of the essential features of the Rust language, use those to motivate the high-level structure of the RustBelt verification, and then go into some depth about Iris, the foundational Coq framework for higher-order concurrent separation logic on top of which RustBelt is built.

Bio:
Derek Dreyer is a professor of computer science at the Max Planck Institute for Software Systems (MPI-SWS), and recipient of the 2017 ACM SIGPLAN Robin Milner Young Researcher Award.  His research runs the gamut from the type theory of high-level functional languages, down to the verification of compilers and low-level concurrent programs under relaxed memory models.  He is currently leading the RustBelt project, which focuses on building the first formal foundations for the Rust programming language.  He also knows a thing or two about Shostakovich and Scotch whisky.