RustBelt: securing the foundations of the Rust programming language

This is a past event

6 people went

Commonwealth Bank of Australia

Level 15, 255 Pitt Street · Sydney

How to find us

This is the office tower above the Hilton. Inside the Hilton lobby, you will see two corridors of elevators: choose the non-carpeted one and proceed to level 15. Please call Mark (0451 158 602) or Rowan (0491 212 140) on arrival.

Location image of event venue

Details

Today we continue reading the RustBelt paper as part of our exploration of type theory in practice.

https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf

Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff 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 paper, we give 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.

A blog post on the paper by Adrian Colyer is at

https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-foundations-of-the-rust-programming-language/