People of ACM - Derek Dreyer

May 20, 2025

Why are formal foundations important for the safety and reliability of software systems?

The problem of developing formal foundations for software systems has been a grand challenge of computer science from the very beginning. First of all, it involves defining the "semantics" of a program: what does the program do when we execute it? Then, once we answer that, how can we establish rigorously that programs work as intended? Can we prove that all programs written in a certain programming language enjoy important properties, e.g. that they are safe to execute? Can we prove that compilers preserve those properties down to machine code? These are pretty basic questions to answer if we want to have high confidence in a complex software system and make sure that all the pieces of the software stack fit together properly. But traditionally, when researchers have studied these questions, they've made simplifying assumptions which idealize away the "dirtier" aspects of real systems and thus open up new attack surfaces.

My work focuses on building formal foundations that avoid these simplifying assumptions in the hope that we can eventually make rigorous claims about the behavior of real-world software systems. A good example would be our work on the RustBelt project, where we built the first formal foundations for the Rust programming language. The reality is that, despite being a “safe” systems programming language, Rust relies on unsafe code in the implementations of its core abstractions which safe code then critically relies upon. It seemed important to us to account properly for Rust's use of unsafe code, since a bug there would undermine its entire safety story. So in RustBelt, rather than sweeping this reality under the rug, we confronted it head-on and developed a new "logical" approach to proving type safety in the presence of unsafe code (see my POPL'18 keynote lecture or our Journal of the ACM article from 2024).

Your most downloaded article in the ACM Digital Library is the 2021 article in Communications of the ACM, “Safe systems programming in Rust” (co-authored with Ralf Jung, Jacques-Henri Jourdan, and Robbert Krebbers) in which you outlined the benefits of the Rust programming language. How does Rust overcome some longstanding challenges in the field? As Rust is open source, how will more people contributing to it improve its effectiveness?

Rust addresses the longstanding challenge of how to support the low-level control and performance of languages like C and C++ while at the same time avoiding the pitfalls of those languages such as memory safety bugs and data races. Major companies like Google and Microsoft have said that such bugs account for around 70% of the major security vulnerabilities in their code bases, so a language that can rule them out at compile time is a big deal.

I think Rust is really exciting because on the one hand it is building on a lot of ideas from research on type systems and language design from the two decades preceding it (particularly surrounding the concept of "ownership"), but on the other hand it puts those ideas together in a novel way and with a keen focus on ergonomics. Such an impactful design did not arise in a vacuum. Rust's open-source development model has been critical to its success, with the language evolving and benefiting enormously from the contributions of thousands of community developers.

Your most cited paper in the ACM DL is the POPL 2015 paper “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning,” which recently received the Most Influential Paper Award at POPL 2025. You, along with co-authors Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, and Lars Birkedal, note that “to scalably verify concurrent programs…we need compositional methods for reasoning about shared state.” How does the Iris separation logic you introduce in this paper address this problem?

Iris builds on a long line of work on separation logic, which was proposed about 25 years ago as a foundation for scalable verification of pointer-manipulating programs. A few years after its inception, Peter O'Hearn and Steve Brookes realized that the core concepts of separation logic—in particular the idea of “ownership”—could significantly simplify reasoning about concurrent, multi-threaded programs as well. Their work (which received the 2016 Gödel Prize) led to the development of many concurrent separation logics (plural), but as a result the field became fractured.

The Iris project grew out of an attempt to unify and consolidate the field: it allows the user to choose their own notion of “ownable resource” that they want to reason about for a particular application, and then provides a powerful set of building blocks with which to soundly derive new proof rules for that application. As a result, Iris has become a widely used tool for experimenting with new kinds of reasoning patterns. For example, we used it in RustBelt to derive the “lifetime logic,” which enabled us in turn to build a semantic model of Rust's lifetime mechanism. Iris is also being used as a key building block in cutting-edge verification projects like Perennial and Verus.

Crucially, Iris is open-source and implemented in The Rocq Prover (formerly Coq). This makes it so that you can build on Iris developments from contributors around the world and you don't have to trust that they are correct because everything is machine-checked in Rocq.

We understand you are a fan of classical music. How did this interest begin?

I don’t know exactly, but most of my childhood memories involve music. My mother was always encouraging my interest in music and dance, and she got me into the children's chorus of the New York City Opera, which was an incredible experience that exposed me to a lot of music I might not otherwise have encountered. I still vividly remember seeing Schoenberg's “Moses und Aron” there when I was 10 years old—it was possibly my first encounter with atonal music, whose transgressiveness definitely appealed to me at the time. But then I discovered a much wider range of composers—especially 20th-century composers like Shostakovich and Britten, whose music is such a moving and deeply personal reflection of the "interesting times" in which they lived. They wrote so much amazing stuff that only a tiny fraction of people in the world have heard (Britten's "Cantata Academica”, anyone?). So, when my 10-year-old daughter Alma goes around the house humming a Shostakovich fugue , I feel I’ve somehow succeeded in life.