Rust is a new language developed at Mozilla Research that marries
together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom. As such, Rust has the potential to
revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having to give
up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally
investigated, and it is not at all clear that they hold. To rule out
data races and other common programming errors, Rust's core type
system prohibits the aliasing of mutable state, but this is too
restrictive for implementing some low-level data structures.
Consequently, Rust's standard libraries make widespread internal use
of "unsafe" blocks, which enable them to opt out of the type system
when necessary. The hope is that such "unsafe" code is properly
encapsulated, so that Rust's language-level safety guarantees are
preserved. But due to Rust's bleeding-edge type system, along with its
reliance on a weak memory model of concurrency, verifying that Rust
and its libraries are actually safe will require fundamental advances
to the state of the art.

In the RustBelt project, funded by an ERC Consolidator Grant, we aim
to build the first formal tools for verifying safety of Rust. To
achieve this goal, we will build on recent breakthrough developments
in the area of concurrent separation logic, which I will explain and
motivate in the talk starting from first principles.