Verified compilers are typically proved correct under severe restrictions on what the compiled code may be linked with, from no linking at all to linking with only the output of the same compiler. Unfortunately, such assumptions don’t match reality. A key challenge when verifying correct compilation of components – or “compositional” compiler correctness – is how to formally state the compiler correctness theorem so it supports linking with target code of arbitrary provenance, as well as verification of multi-pass compilers. Recent results state their correct-component-compilation theorems in remarkably different ways, yielding pros and cons that aren’t well understood.

I will survey recent work on compiler verification, explaining the high-level essence of their compiler correctness formalisms and the latter’s impact on proof effort, modular verification, and usefulness of the theorems. I’ll discuss what a generic compositional compiler correctness theorem might look like and what it reveals about desired properties of proof architectures going forward. I’ll argue that compositional compiler correctness is, in essence, a language interoperability problem: embedding a single-language fragment in a multi-language system affects the notion of program equivalence that programmers use when reasoning about their code and that compiler writers use when reasoning about the correctness of compiler optimizations. For better compiler verification results in the long term, we must consider designing languages that give programmers control over a range of interoperability (linking) options.

The lecture will be 3 hours and a half, on Tuesday.

My research involves the use of programming-language semantics and type systems for reasoning about imperative code, security, concurrency, compiler transformations, and provenance. My present focus is on how to build verified compilers that ensure safe linking of code compiled from different programming languages. This includes work on correct and secure compilation, gradual typing, dependent types, and safe language interoperability.