I just got started with the software foundations that is currently in beta which walks you through the Verificable C project. It’s super cool! I do have one sort of general question: in practice, where does CompCert fall short?
That is to say, let’s say someone needs to use C for some reason…why would they go to gcc or clang over compcert? Compilation speed? Quality of optimizations? Linker option? Unsupported parts of the language? Just want to get a handle on what the limitations are for a project like this are in practice because honestly, it seems super awesome and like a really heroic undertaking.
It sounds like you’re asking why a C programmer wouldn’t switch to CompCert (as opposed to someone building verification infrastructure that interfaces with CompCert in some way). There are many reasons why you’d want to use a production compiler. As you’ve said, CompCert is a heroic undertaking and an amazing achievement. There are many features in gcc and clang which come from having probably a thousand times more engineering effort than CompCert, and of course these engineers did not also have to prove correctness.
- Essentially everything you mentioned: compilation speed and optimizations are really important. If you’re a big tech company, 3% faster code on average means a 3% reduction in the operating cost of your software, and that might just be the difference between gcc and LLVM. The monetary cost of compiler bugs is likely to be extremely small, if not zero. Of course this depends on what you use the software for: the risk of a critical and undetected miscompilation might be more likely or higher cost in some applications.
- As you mentioned gcc and clang support a much larger language, including features that companies rely on but aren’t even part of the C standard.
- gcc and clang have many features for developing software and not just compiling it, like good error messages, debug symbols, and compiling with profiling-related information. They also support a million architectures and environments, things like
-ffreestanding where gcc/clang do not assume you have an operating system. (Note that CompCert also supports the common architectures, including ARM, RISC-V, and PowerPC.)
- gcc and clang have been debugged carefully. If you’re not following the C standard, then in practice this might be more important to you than knowing the compiler faithfully compiles legal C code. There’s a tradeoff here since gcc and clang also might at any point do strange things to your code if it has undefined behavior. This argument doesn’t really apply to verification toolchains that prove something on top of the CompCert specification, in which case the application has been verified to not have undefined behavior as defined by CompCert.
Thank you so much for the answer!
I guess I was wondering why a new C project wouldn’t consider CompCert…the hope of porting seems basically 0, but I was wondering why it wouldn’t be in the running for new projects.
I asked a friend who writes a lot of C professionally and he said a lot of the missing language features would already be show stoppers, but more generally was suspicious of the value, which I thought was a shame (basically, he felt that dynamic analysis would get more of the reward without having to switch to an inferior tool chain and engage in a bunch of very difficult proofs).
The point about gcc and clang being about software development and not just compilation is also a good one. But they’re all good points
At some point I want to try to do something smallish but non-trivial in verified C and see how much of a bear it is…
Edit: I guess there are also some contexts where the costs of failure are very, very high. While I would never want to support military applications, an F35 for example which costs like a billion dollars. Or space probes. Perhaps in practice the things which sink this could not be helped by compcert (and something like verified C). I know that they have extremely laborious code review and testing standards, though.