Next Meetup

RustBelt: securing the foundations of the Rust programming language
Today we continue reading the RustBelt paper as part of our exploration of type theory in practice. 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

Commonwealth Bank of Australia

Level 15, 255 Pitt Street · Sydney

What we're about

Let's get together and learn about type theory!

We're a type theory reading group in Sydney, Australia. Inspired by the online type theory study group (, our focus is type theory with a view towards programming languages.

We're currently reading Simon Thompson's Type Theory and Functional Programming (

In the past we read much of Bob Harper's "Practical Foundations for Programming Languages", 2nd Edition (, with some excursions into other topics, including modal type theory and linear types, as well as implementations in Twelf and Idris. Our resident expert is Rowan Davies (

Some videos of past sessions are available via the following link, including two catch up sessions (highly recommended for new members): (

Members (241)

Photos (10)