Distinguished Lecture Series: Derek Dreyer




"RustBelt: Logical Foundations for the Future of Safe Systems Programming"

Derek Dreyer
Max Planck Institute for Software Systems (MPI-SWS)

Thursday, May 12, 2016
3:00 pm, Ryerson 251

*Reception to follow in Ryerson 255 at 4:00 pm*

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 actually hold. To
rule out data races and other common programming errors, Rust's core
type system prohibits the aliasing of mutable state.  This is too
restrictive, however, for a number of essential data structures, and
thus Rust's standard libraries make widespread internal use of
"unsafe" features of the language.  The Rust developers claim that
such "unsafe" code has been properly encapsulated, so that Rust's
language-level safety guarantees are preserved.  But this claim is
called into question by various subtle safety bugs uncovered in Rust
in the past year.

In the RustBelt project, we aim to develop the first formal
foundations for the safety of Rust programs.  To tackle this
challenge, we will build on recent breakthrough developments in the
area of Concurrent Separation Logic, in particular our work on the
Iris and GPS program logics.  In the talk, I will explain what
Concurrent Separation Logic is, why it is relevant to the Rust
verification effort, what problems remain in developing a program
logic suitable for Rust, and how Iris and GPS make progress toward
that goal.

About the Speaker:
Derek Dreyer heads the Foundations of Programming Group at the Max
Planck Institute for Software Systems (MPI-SWS) in Saarbruecken,
Germany, where he has been a member of the faculty since 2008 and
received tenure in 2013.  He was previously a research assistant
professor at Toyota Technological Institute at Chicago, after
receiving his PhD from CMU in 2005.  He is a member of the editorial
board of the Journal of Functional Programming, and was elected to
serve on the ACM SIGPLAN Executive Committee from 2012 to 2015.

Dr. Dreyer's research focuses on building foundations for modular,
scalable verification of programs in *realistic* programming languages
-- languages that combine complex features (e.g. closures, abstract
data types, ownership types, weak-memory concurrency) in poorly
understood ways.  Toward this end, he has recently been awarded a
2-million-euro Consolidator Grant from the European Research Council
for the project RustBelt, concerning the development of rigorous
formal foundations for safe systems programming in the Rust language.

Host: John Reppy

For more information about future and/or past Distinguished Lectures, please visit: Distinguished Lecture Series