[Blog] CompCert #547
[Blog] CompCert #547
Conversation
| 2. Producing a correct output | ||
| 3. Crashing or "going wrong" during execution (such as accessing an array out of bounds) | ||
|
|
||
| Generally, programmers expect a slightly relaxed version of "always producing the same behavior." Particularly, because crashing behaviors can sometimese be optimized away, we care most about producing correct outputs and termination behavior. This leads us to our property of semantic preservation |
| With these tools, we can now tackle proving semantic preservation using a number of approaches. CompCert uses $3$ general approaches to these proofs: | ||
|
|
||
| ### Verified compilers | ||
| The first and generally most complex method is writing fully verified compiler code. This means that we apply proof assistant tools to thte compiler source itself, ensuring that the compiler itself maintains specifications. |
|
|
||
| ### Proof-carrying code and certifying compilers | ||
|
|
||
| The final method uses the approach of proof-carrying code (PCC). PCC uses a *certifying compiler*, which is a compiler $CComp$ that produces a result $C$ along with a proof $\pi$ (the certificate) of the property $C \vDash \text{Spec}$. Therefore, a verified compiler can be constructed from a certifying compiler by formally verifying a client-side proof checker. |
There was a problem hiding this comment.
Maybe it would be nice to include (here or later) one sentence about which of these approaches CompCert takes, at a high level, and why it picked one or the other.
| Note that this is different from the original subset described in the CompCert paper, which instead compiles from Clight, a subset of C that excludes more features such as extended-precision arithmetic and arbitrary control flow through `goto`. | ||
|
|
||
| The formally verified CompCert compiler translates from CLight to PowerPC abstract syntax. |
There was a problem hiding this comment.
This is a little confusing because it switches between describing "CompCert as depicted in the paper" and "CompCert as of May 2025." Maybe this could use a little more explicitness about which situation applies to which.
| 1. The parsing pass of the compiler | ||
| 2. Assembling and linking | ||
| 3. Coq and its proof assistant algorithms must be correct | ||
| 4. The Coq to Caml extractor (and thus Caml's compiler) |
| 3. Coq and its proof assistant algorithms must be correct | ||
| 4. The Coq to Caml extractor (and thus Caml's compiler) | ||
| 5. PowerPC specifications being accurate (for the specific chips used) | ||
| 6. Developer software! |
There was a problem hiding this comment.
What is "developer software"? Do you mean the input program? If so, I think this belongs in a different category than the TCB of the compiler itself…
| 5. PowerPC specifications being accurate (for the specific chips used) | ||
| 6. Developer software! | ||
|
|
||
| Although this seems like still many different points of weakness, existing projects are actively formally verifying Coq and sthe Coq to OCaml extractor. There also exists work to create a verified Caml to C#minor compiler, which takes care of the Caml compiler. |
| 2. `longjmp` and `setjmp`, which allow for non-local jumps (jumps into different program contexts). | ||
| 3. Variable-length arrays. | ||
|
|
||
| Note that this is different from the original subset described in the CompCert paper, which instead compiles from Clight, a subset of C that excludes more features such as extended-precision arithmetic and arbitrary control flow through `goto`. |
There was a problem hiding this comment.
When you first introduce the fact that you are discussing a paper, it would be a good idea to link to that paper.
|
Hi, @UnsignedByte @mse63 @Jonahcb! I would love to publish your blog post. Can you please wrap up the revisions discussed above so I can hit the green button? |
|
Just one last reminder about the above, @UnsignedByte @mse63 @Jonahcb—if you don't want to wrap up the small additions above, we can just close this PR. |
Sorry about the late submission, totally did not realize that we had to make a blog post.