1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
+++
title = "CompCert "
date = "2020-12-10"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b6", "1f2a", "1d1", "1b2"]
forwardlinks = ["3a4", "3b", "3a1"]
zettelid = "3a"
+++
CompCert \[1\] is a formally verified C compiler, meaning it has been
proven to always generate machine code that behaves in the same way as
the original C code. It therefore cannot have any bugs, as every
translation step has a proof that it is correct. This proof is encoded
in a theorem prover called Coq, and unlike many other proofs, the
compiler itself is also written in Coq, so the proof corresponds
directly to the algorithms. The proofs that are performed in the
compiler are described in ([\#3a4]).
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-leroy09_formal_verif_realis_compil" class="csl-entry"
markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">X. Leroy, “Formal verification of
a realistic compiler,” *Commun. ACM*, vol. 52, no. 7, pp. 107–115, Jul.
2009, doi: [10.1145/1538788.1538814].</span>
</div>
</div>
[\#3a4]: /zettel/3a4
[10.1145/1538788.1538814]: https://doi.org/10.1145/1538788.1538814
|
