Comment by UncleMeat

11 days ago

Because people want a performant optimizing compiler.

CompCert produces surprisingly fast native code.

This 2022 article [0] says it generates binaries that run about 7% slower than what GCC produces with -O1.

[0] https://www.cs.cornell.edu/courses/cs6120/2022sp/blog/compce...

  • That's a big gap, especially with the norm for releases being O2 if I understand correctly.

    • > That's a big gap

      I wouldn't say so. The gap between GCC and Clang/LLVM is bigger than that on some benchmarks, [0] although the gap between their overall performance (using geometric mean) is much less. [1]

      It's a very impressive result considering how much effort has gone into GCC. It highlights how compiler optimisation work can face diminishing returns.

      > the norm for releases being O2 if I understand correctly

      Agreed, but the difference isn't that great. From the article:

      > CompCert code is 7% slower than gcc-01 and 12% slower than gcc-02 on average.

      Reminds me of how the cproc/qbe C compiler gets very roughly 50% of the performance of Clang/LLVM in 0.1% the lines-of-code. [2]

      [0] https://www.phoronix.com/review/gcc-16-vs-clang-22/3

      [1] https://www.phoronix.com/review/gcc-16-vs-clang-22/6

      [2] https://drewdevault.com/talks/qbe/ (and see the linked slideshow PDF, as the abstract is a little misleading)

      2 replies →