Compiler correctness is an old problem, with results stretching back beyond the last half-century and particularly impressive results such as CompCert over the last decade and a half. And yet, until quite recently, the theorems being proved were only about the compilation of whole programs, a theoretically appealing but practically unrealistic simplification since, in practice, compilers aren’t typically used to compile whole programs, but to compile components that are then linked with other components, even some written in other languages and compiled by different compilers.

There has been much recent work on “compositional” compiler correctness which tackles correct compilation of components. In this talk, I will survey recent results, explaining pros and cons of their different approaches to stating compiler correctness. These remarkably different ways of stating compiler correctness raises questions about what researchers even mean by a “compiler is correct.” I’ll briefly discuss a new framework for compositional compiler correctness (CCC) that helps us assess the relative strengths and weaknesses of recent results and helps provide insight into what we as a community should want from compiler correctness theorems of the future.

This talk will be live-streamed on YouTube here.