The CompCert C Compiler

Original Article ↗ Hacker News Discussion ↗

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.