Review: Formal verification of a realistic compiler
High Level Summary
In this paper, the author discusses how they built CompCert, a formally verified Clight compiler with Coq. Formally verified compilers are important for safe-critical software engineering, because it enables the verification of programs to be done at the source code level, and eliminates the need of manually verifying machine code. The verified compiler compiles the parsed Clight language into 8 intermediate languages in 14 steps, each of which is written and verified in Coq. The author also describes in detail how to register allocation stage is written and proved as an example.
This is a concise and effective paper that shows in detail how formal methods can be applied in real world programming. The paper shows a very clear structure — formally defining the “correctness” (semantic preservation) property in section 2, gives an overview of the compiler in section 3, and goes into a specific stage of the compiler to demonstrate how the compiler works. It feels like an engineering paper, but shows how theory can be directly applied to a very common real-world task — compiling C code, with reasonable performance. I’m a bit surprised (though I probably shouldn’t be) that Coq can produce runnable Caml code that can have real world uses. Overall, this paper makes me feel that theory is not that distant from real world applications.
Overall, I think this paper is very well-written, with an appropriate length and a clear structure. As an engineering paper with open source code, I would say that the point the author has is pretty strong — yes, formally proved compilers are possible. Limitations, if any, is what the author mentions in section 5. The current (at the time of writing) CompCert still relies on some external assumptions like the formal semantics of Clight itself, the parser, the assembler, the linker, etc.