Type systems—and the associated concept of “type soundness”—are one of the biggest success stories of foundational PL research. Originally proposed by Robin Milner in 1978, type soundness asserts that well-typed programs can’t “go wrong” (i.e., exhibit undefined behaviors), and it is widely viewed as the canonical theorem one must prove to establish that a type system is doing its job. In the early 1990s, Wright and Felleisen introduced a simple syntactic approach to proving type soundness, which was subsequently popularized as the method of “progress and preservation” and has had a huge impact on the study and teaching of PL foundations. Many research papers that propose new type systems conclude with a triumphant statement of syntactic type soundness, and for many students it is the only thing they learn to prove about a type system.

Unfortunately, syntactic type soundness is a rather weak theorem. First of all, its premise is too strong for many practical purposes. It only applies to programs that are completely well-typed, and thus tells us nothing about the many programs written in “safe” languages that make use of “unsafe” language features. Even worse, it tells us nothing about whether type systems achieve one of their main goals: enforcement of data abstraction. One can easily define a language that enjoys syntactic soundness and yet fails to support even the most basic modular reasoning principles for closures, objects, and ADTs.

In this talk, I argue that we should no longer be satisfied with just proving syntactic type soundness, and should instead start proving a stronger theorem—semantic type soundness—that captures more accurately what type systems are actually good for. In a semantic soundness proof, one defines a semantic model of types as predicates on values, and then verifies the soundness of typing rules as lemmas about the model. By explaining directly what types “mean”, the semantic approach to type soundness is a lot more informative than the syntactic one. In particular, it can serve to establish what data abstraction guarantees a language provides, as well as what it means for uses of unsafe language features to be “safely encapsulated”.

Semantic type soundness is a very old idea—Milner’s original formulation of type soundness was a semantic one—but it fell out of favor in the 1990s due to limitations and complexities of denotational models. In the succeeding decades, such limitations have been overcome and complexities tamed, via proof techniques that work directly over operational semantics. Thanks to the development of step-indexed Kripke logical relations, we can now scale semantic soundness to handle real languages, and thanks to advances in higher-order concurrent separation logic, we can now build (machine-checked) semantic soundness proofs at a much higher level of abstraction than was previously possible. The resulting “logical” approach to semantic type soundness yields proofs that are demonstrably more useful than their syntactic counterparts, and more fun as well.

Derek Dreyer is a professor of computer science at the Max Planck Institute for Software Systems (MPI-SWS), and recipient of the 2017 ACM SIGPLAN Robin Milner Young Researcher Award. His research runs the gamut from the type theory of high-level functional languages, down to the verification of compilers and low-level concurrent programs under relaxed memory models. He is currently leading the RustBelt project, which focuses on building the first formal foundations for the Rust programming language. He also knows a thing or two about Scotch whisky.