Notes on Compiler Correctness

A compiler is a function from programs to programs. Correctness means the output program has the same observable behavior as the input program, for all possible inputs. This is a deceptively simple statement with deep consequences.

What "Same Behavior" Means

Observable behavior is defined by the source language semantics. If the source language has undefined behavior, the compiler is free to do anything with those programs. This is not a bug — it is a feature that enables optimization. But it means correctness is relative to a formal specification that may not match the programmer's expectations.

The CompCert Approach

CompCert proves correctness by establishing a simulation relation between the source and target programs. Each step of the target program corresponds to zero or more steps of the source program, and the observable events (I/O, memory accesses) match.

A verified compiler does not eliminate bugs. It eliminates one class of bugs — miscompilation — with mathematical certainty. Every other class remains.

The Cost of Verification

CompCert's proof is approximately 100,000 lines of Coq. The compiler itself is far smaller. This ratio — proof to code — is typical of verified systems and raises a practical question: is the cost justified?

For most software, probably not. But for safety-critical systems — avionics, medical devices, nuclear control — the cost of a miscompilation bug exceeds the cost of formal verification by orders of magnitude.

---

Compiler correctness is a solved problem in theory. In practice, it remains a matter of economics and risk tolerance.