Translation validation of compilers.
In compilation, especially optimising compilation, correctness is a big issue for obvious reasons.
Ideally, we'd like the whole compiler being proven correct once and for all, but this is beyond the state-of-the-art in 2023 for
industrial strength compilers like LLVM and GCC (still there is progress, see CompCert [1]
CakeML [2]).
However, we should not let the perfect be the enemy of the good: enter translation validation [3]. The idea is simple:
instead of giving a single proof that the compiler is correct for all input programs $P$, we prove, for an individual program $P$ that the translation of
$P$ is correct. This is much less demanding. Note that proving that the compiler correctly translates a given program $P$, does not imply that it
also translates other programs correctly! That may sound really weak, but, empirically, translation validation is useful [4, 5, 6]:
Translation validation (at least of individual optimisation passes) can be automated with SMT solvers like Z3, even for complex LLVM optimisation passes.
Doing translation validation for a modest size number of programs finds huge number of bugs in complex LLVM optimisation passes automatically
This raises more questions: for example, is the translation validator itself correct? See [7] for recent progress in this direction.
[1] X. Leroy, Formal verification of a realistic compiler. https://xavierleroy.org/publi/compcert-CACM.pdf
[2] https://cakeml.org/
[3] A. Pnueli, M. Siegel, E. Singerman, Translation Validation.
[4] N. P. Lopes, D. Menendez, S. Nagarakatte, J. Regehr, Provably Correct Peephole Optimizations with Alive.
[5] N. P. Lopes, J. Lee, C.-K. Hur, Z. Liu, J. Regehr, Alive2: Bounded Translation Validation for LLVM.
[6] https://github.com/AliveToolkit/alive2
[7] J. Lee, C.-K. Hur, N. P. Lopes, AliveInLean: A Verified LLVM Peephole Optimization Verifier.