4 ms·

Can someone explain why CompCert is not more popular? A formally verified compiler seems to be much more useful than something that can produce bugs.

dkarapetyan 13y ago
For one you can still write buggy software in it and for another there are some limitations that can be potential deal breakers: http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html. That links spells out some of the limitations.
ahomescu1 13y ago
It doesn't support all of C99 [1]. In real-world code, you need that, plus the GNU extensions (the clang developers put in a lot of work into making clang fully compatible with gcc, going as far as accepting the same command-line switches). 1 - http://compcert.inria.fr/compcert-C.html#subset http://compcert.inria.fr/compcert-C.html#subset
- nullc 13y ago
  Considering that the parts of C99 that it doesn't support are also not supported by MSVC I can't imaging that that alone is much of a big deal. The prohibition on commercial use is a much bigger barrier, I expect.
  - ahomescu1 13y ago
    MSVC supports C++ instead (AFAIK, it has most of C++11 implemented), while CompCert doesn't compile C++ at all.
vilhelm_s 13y ago
It's not free software (the license permits educational and research but commercial use). I guess selling compilers to people is a hard problem in itself. :)
cwzwarich 13y ago
Even ignoring the licensing issues and limited subset of C supported, the code quality doesn't approach that of modern optimizing compilers, and the correctness proof doesn't include things like concurrency or actual machine memory models (although forks of CompCert exist for some of these), so you're still off in the unverified world if you rely on them in your code. Also, for the vast majority of programs the possibility of bugs in the compiler is not really that impactful in terms of total effect on reliability.
- Igglyboo 13y ago
  The article said something about being as good as GCC with O1, is that not enough? Pardon my ignorance, I've never touched c/c++ (python guy).
  - betterunix 13y ago
    1. O3 is way better. 2. GCC is not even the best optimizing compiler out there. Intel's C compiler puts GCC to shame for some tasks.
andor 13y ago
It's not a drop-in replacement for gcc. For example: In the second form above, main is called with argc equal to zero and argv equal to the NULL pointer. The program does not, therefore, have access to command-line arguments. http://compcert.inria.fr/man/manual004.html#toc11 http://compcert.inria.fr/man/manual004.html#toc11

dkarapetyan 13y ago

For one you can still write buggy software in it and for another there are some limitations that can be potential deal breakers: http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html. That links spells out some of the limitations.

ahomescu1 13y ago

It doesn't support all of C99 [1]. In real-world code, you need that, plus the GNU extensions (the clang developers put in a lot of work into making clang fully compatible with gcc, going as far as accepting the same command-line switches). 1 - http://compcert.inria.fr/compcert-C.html#subset http://compcert.inria.fr/compcert-C.html#subset

nullc 13y ago
Considering that the parts of C99 that it doesn't support are also not supported by MSVC I can't imaging that that alone is much of a big deal. The prohibition on commercial use is a much bigger barrier, I expect.
- ahomescu1 13y ago
  MSVC supports C++ instead (AFAIK, it has most of C++11 implemented), while CompCert doesn't compile C++ at all.

vilhelm_s 13y ago

It's not free software (the license permits educational and research but commercial use). I guess selling compilers to people is a hard problem in itself. :)

cwzwarich 13y ago

Even ignoring the licensing issues and limited subset of C supported, the code quality doesn't approach that of modern optimizing compilers, and the correctness proof doesn't include things like concurrency or actual machine memory models (although forks of CompCert exist for some of these), so you're still off in the unverified world if you rely on them in your code. Also, for the vast majority of programs the possibility of bugs in the compiler is not really that impactful in terms of total effect on reliability.

Igglyboo 13y ago
The article said something about being as good as GCC with O1, is that not enough? Pardon my ignorance, I've never touched c/c++ (python guy).
- betterunix 13y ago
  1. O3 is way better. 2. GCC is not even the best optimizing compiler out there. Intel's C compiler puts GCC to shame for some tasks.

andor 13y ago

It's not a drop-in replacement for gcc. For example: In the second form above, main is called with argc equal to zero and argv equal to the NULL pointer. The program does not, therefore, have access to command-line arguments. http://compcert.inria.fr/man/manual004.html#toc11 http://compcert.inria.fr/man/manual004.html#toc11