UnderstandingandEvolvingthe
     RustProgrammingLanguage
     Derek Dreyer
     MPI-SWS, Germany
     Collège de France
     February 6, 2020
                                                        1
   Rust–Mozilla’sreplacementforC/C++
     Rust is the only language to provide...
     • Low-level control à la C/C++
     • Strong safety guarantees
     • Modern, functional paradigms
     • Industrial development and backing
     Core ingredients:
     • Sophisticated ownership type system
     • Safe encapsulation of unsafe code
                                                        2
   Rust–Mozilla’sreplacementforC/C++
     Rust is the only language to provide...
     • Low-level control à la C/C++
     • Strong safety guarantees
     • Modern, functional paradigms
     •         Goal of RustBelt project:
       Industrial development and backing
           Build first formal foundations
     Core ingredients:
     •          for the Rust language!
       Sophisticated ownership type system
     • Safe encapsulation of unsafe code
                                                        2
     Understanding Rust: λRust
     Building an extensible soundness proof of Rust that
     covers its core type system as well as standard libraries
     Evolving Rust: Stacked Borrows
     DefiningthesemanticsofRustinordertojustify
     powerful intraprocedural type-based optimizations
                                                        3