Compiler correctness is an old problem, with results stretching back + beyond the last half-century. Founding the field, John McCarthy and James + Painter set out to build a "completely trustworthy compiler". And yet, + until quite recently, even despite truly impressive verification efforts, + the theorems being proved were only about the compilation of whole + programs, a theoretically quite appealing but practically unrealistic + simplification. For a compiler correctness theorem to assure complete + trust, the theorem must reflect the reality of how the compiler will be + used.
+There has been much recent work on more realistic "compositional" + compiler correctness aimed at proving correct compilation of components + while supporting linking with components compiled from different + languages using different compilers. However, the variety of theorems, + stated in remarkably different ways, raises questions about what + researchers even mean by a "compiler is correct." In this pearl, we + develop a new framework with which to understand compiler correctness + theorems in the presence of linking, and apply it to understanding and + comparing this diversity of results. In doing so, not only are we better + able to assess their relative strengths and weaknesses, but gain insight + into what we as a community should expect from compiler correctness + theorems of the future.
+ +Compiler correctness is an old problem, with results stretching back + beyond the last half-century. Founding the field, John McCarthy and James + Painter set out to build a "completely trustworthy compiler". And yet, + until quite recently, even despite truly impressive verification efforts, + the theorems being proved were only about the compilation of whole + programs, a theoretically quite appealing but practically unrealistic + simplification. For a compiler correctness theorem to assure complete + trust, the theorem must reflect the reality of how the compiler will be + used.
+There has been much recent work on more realistic "compositional" + compiler correctness aimed at proving correct compilation of components + while supporting linking with components compiled from different + languages using different compilers. However, the variety of theorems, + stated in remarkably different ways, raises questions about what + researchers even mean by a "compiler is correct." In this pearl, we + develop a new framework with which to understand compiler correctness + theorems in the presence of linking, and apply it to understanding and + comparing this diversity of results. In doing so, not only are we better + able to assess their relative strengths and weaknesses, but gain insight + into what we as a community should expect from compiler correctness + theorems of the future.
+ +