CIL-based parser, the assembler, and the linker.
3. The compilation chain used to produce the executable
for the compiler: Coq’s extraction facility and the Caml
compiler and run-time system. (A bug in this compilation chain could invalidate the guarantees obtained by
the correctness proof.)
4. The Coq proof assistant itself. (A bug in Coq’s implementation or an inconsistency in Coq’s logic could falsify the proof.)
Issue ( 4) is probably the least concern: as Hales argues, 10
proofs mechanically checked by a proof assistant that generates proof terms are orders of magnitude more trustworthy than even carefully hand-checked mathematical
To address concern ( 3), ongoing work within the
CompCert project studies the feasibility of formally verifying Coq’s extraction mechanism as well as a compiler
from Mini-ML (the simple functional language targeted by
this extraction) to Cminor. Composed with the CompCert
back-end, these efforts could eventually result in a trusted
execution path for programs written and verified in Coq,
like CompCert itself, therefore increasing confidence further through a form of bootstrapping.
Issue ( 2) with the unverified components of CompCert
can obviously be addressed by reimplementing and proving the corresponding passes. Semantic preservation for
a parser is difficult to define, let alone prove: what is the
semantics of the concrete syntax of a program, if not the
semantics of the abstract syntax tree produced by parsing? However, several of the post-parsing elaboration steps
performed by CIL are amenable to formal proof. Likewise,
proving the correctness of an assembler and linker is feasible, if unexciting.
Perhaps the most delicate issue is ( 1): how can we
make sure that a formal semantics agrees with language
standards and common programming practice? Since
the semantics in question are small relative to the whole
compiler, manual reviews by experts, as well as testing conducted on executable forms of the semantics, could provide
reasonable (but not formal) confidence. Another approach
is to prove connections with alternate formal semantics
independently developed, such as the axiomatic semantics
that underline tools for deductive verification of programs
(see Appel and Blazy for an example). Additionally, this
approach constitutes a first step towards a more ambitious,
long-term goal: the certification, using formal methods, of
the verification tools, code generators, compilers and run-time systems that participate in the development, validation and execution of critical software.
The author thanks S. Blazy, Z. Dargaye, D. Doligez,
B. Grégoire, T. Moniot, L. Rideau, and B. Serpette for their
contributions to the CompCert development, and A. Appel,
Y. Bertot, E. Ledinot, P. Letouzey, and G. Necula for their
suggestions, feedback, and help. This work was supported
by Agence Nationale de la Recherche, grant number ANR-
1. Appel, A. W. Foundational proof-carrying code. In Logic in Computer
Science 2001 (2001), IEEE, 247–258.
2. Appel, A. W., Blazy, S. Separation
logic for small-step Cminor. In
Theorem Proving in Higher Order
Logics, TPHOLs 2007, volume 4732
of LNCS (2007), Springer, 5–21.
3. Bertot, Y., Castéran, P. Interactive
Theorem Proving and Program
Development—Coq’Art: The Calculus
of Inductive Constructions (2004),
4. Blazy, S., Dargaye, z., Leroy, X.
Formal verification of a C compiler
front-end. In FM 2006: International
Symposium on Formal Methods,
volume 4085 of LNCS (2006),
5. Blazy, S., Leroy, X. Mechanized
semantics for the Clight subset of
the C language. J. Autom. Reasoning
(2009). Accepted for publication, to
6. Chaitin, G.J. Register allocation and
spilling via graph coloring. In 1982
SIGPLAN Symposium on Compiler
Construction (1982), ACM, 98–105.
7. Coq development team. The Coq
proof assistant. Available at http://
8. Dave, M.A. Compiler verification: a
bibliography. SIGSOFT Softw. Eng.
Notes 28, 6 (2003), 2.
9. George, L., Appel, A. W. Iterated
register coalescing. ACM Trans. Prog.
Lang. Syst. 18, 3 (1996), 300–324.
10. hales, T.C. Formal proof. Notices
AMS 55, 11 (2008), 1370–1380.
11. Leroy, X. Formal certification of a
compiler back-end, or: programming
a compiler with a proof assistant. In
33rd Symposium on the Principles
of Programming Languages (2006),
12. Leroy, X. The CompCert verified
compiler, software and commented
proof. Available at http://compcert.
inria.fr/, Aug. 2008.
13. Leroy, X. A formally verified compiler
back-end. arXiv:0902.2137 [cs].
Submitted, July 2008.
14. Leroy, X., Blazy, S. Formal
verification of a C-like memory
model and its uses for verifying
program transformations. J. Autom.
Reasoning 41, 1 (2008), 1–31.
Xavier Leroy ( firstname.lastname@example.org) INRIA
15. Letouzey, P. Extraction in Coq: An
overview. In Logic and Theory of
Algorithms, Computability in Europe,
CiE 2008, volume 5028 of LNCS
(2008), Springer, 359–369.
16. McCarthy, J., Painter, J. Correctness
of a compiler for arithmetical
expressions. In Mathematical
Aspects of Computer Science,
volume 19 of Proceedings of
Symposia in Applied Mathematics
(1967), AMS, 33–41.
17. Milner, R., Weyhrauch, R. Proving
compiler correctness in a
mechanized logic. In Proceedings
of 7th Annual Machine Intelligence
Workshop, volume 7 of Machine
Intelligence (1972), Edinburgh
University Press, 51–72.
18. Morrisett, G., Walker, D., Crary, k.,
Glew, N. From System F to typed
assembly language. ACM Trans.
Prog. Lang. Syst. 21, 3 (1999),
19. Necula, G.C. Proof-carrying code. In
24th Symposium on the Principles
of Programming Languages (1997),
20. Necula, G.C. Translation validation
for an optimizing compiler. In
Programming Language Design and
Implementation 2000 (2000), ACM,
21. Necula, G.C., McPeak, S., Rahul,
S.P., Weimer, W. CIL: Intermediate
language and tools for analysis and
transformation of C programs. In
Compiler Construction, volume 2304
of LNCS (2002), Springer, 213–228.
22. Pnueli, A., Siegel, M., Singerman,
E. Translation validation. In Tools
and Algorithms for Construction
and Analysis of Systems, TACAS
‘ 98, volume 1384 of LNCS (1998),
23. Tristan, J.-B., Leroy, X. Formal
verification of translation validators:
A case study on instruction
scheduling optimizations. In 35th
Symposium of the Principles of
Programming Languages (2008),
24. Tristan, J.-B., Leroy, X. Verified
validation of lazy code motion.
In Programming Language
Design and Implementation
2009 (2009), ACM.
© 2009 ACM 0001-0782/09/0700 $10.00