The CompCert C Compiler

Original Article ↗ Hacker News Discussion ↗

A formally verified C compiler like CompCert promises stronger guarantees that compiled machine code faithfully implements C source, but engineers point out that such proofs only cover what’s modeled—unverified subsystems, unsafe APIs, and undefined behavior in C remain major failure sources. Commenters debate whether mission- and safety‑critical software should still be written in C at all, given its pervasive memory‑safety pitfalls, arguing over incremental fixes such as bounds‑checked arrays, annotations, and safer C dialects versus wholesale migration to languages like Rust or Zig. The thread also notes practical barriers to wider use of tools like CompCert, including licensing, limited language feature coverage, and the vast legacy of existing C code.

Formal verification and real-world failures

  • Spacecraft anecdote: a formally model-checked subsystem found a deadlock bug, but a similar bug was later reintroduced in an unverified subsystem and via a direct call that bypassed the verified API.
  • Takeaway in the thread: the verification itself worked; the process and enforcement around it failed.
  • Several comments argue this is more a cautionary tale about bypassing verified interfaces and not applying formal methods “all the way down” than about the weakness of verification itself.

Limits and value of formal methods

  • Formal methods (model checking, Coq/Isabelle, etc.) provide strong guarantees but only over the modeled/verified subset.
  • Scope restrictions (e.g., bounded integers, partial subsystems) are necessary; people warn against treating formal proofs as infallible replacements for engineering care.
  • Verified tools like CompCert are seen as components in a larger verified toolchain, not as complete solutions.

C language safety, arrays, and undefined behavior

  • Large debate over C’s conflation of pointers and arrays and its role in buffer overflows and security issues.
  • Some advocate making arrays distinct, size-tracking types with default bounds checks (fat pointers/slices, safer array syntax, or new “safe array” types).
  • Others counter that this would effectively create a new language, break huge amounts of existing code, and conflict with C’s ABI and “portable assembly” role.
  • Multiple partial remedies are mentioned: C99 variable-length-array annotations, toolchain warnings, sanitizers, compiler extensions and annotations for bounds, and static analysis.
  • Broader criticism targets C’s undefined behavior model, weak standard library, and long-standing safety pitfalls; some argue compilers now exploit UB too aggressively.
  • Counterpoint: C has been used extensively in life- and safety-critical systems with relatively few catastrophic incidents, provided strict processes, coding standards (e.g., MISRA-like), and heavy testing are applied.

Alternatives and ecosystem evolution

  • Rust, Zig, D, and C++ are cited as “better C” options with safer defaults and richer abstractions; Rust is seen as displacing C++ more than C, while Zig is positioned as a gradual C replacement.
  • There is skepticism that the C standard will ever make breaking safety improvements; many expect C to slowly become mostly legacy while newer systems code moves to other languages.

CompCert-specific notes

  • CompCert is praised as a formally verified optimizing C compiler used in high-integrity contexts (e.g., seL4), but it does not make C itself “safe”.
  • Certain features (e.g., setjmp/longjmp) may work but are outside the proof; they’re functionally available but not correctness-verified.
  • Licensing is non-commercial by default, with a commercial path via a vendor.
  • Practical issues reported include high memory use on large codebases and friction around unsupported extensions.