Hacker News new | ask | show | jobs
by pdw 4702 days ago
It seems like they might like CompCert. An optimizing C compiler that comes with a formal proof of correctness. Downsides: GPL, doesn't quite implement the full C language (but it's getting closer), and no support for ancient crap such as m88k.

EDIT: I misunderstood the license file, the majority of the code is non-commercial-use only, only a small part is dual-licensed. Still a cool project, even if it's not open source...
2 comments
pascal_cuoq 4702 days ago
The OP's problem is with the support for the exotic targets and the more recent additions to the C standard (C99, soon C11). CompCert targets only x86 and PowerPC, and does not support all the features of C99, not to mention the GCC extensions that everyone has come to rely on. In fact, in terms of these criteria it is uniformly worse than GCC 2.7.2.1 (although it is better at having verified, bug-free semantics).
link
pdw 4701 days ago
That was only his second complaint.

  "First, compilers are fragile. While one would like to expect a minimum
  level of correctness and trustworthiness from a modern compiler, we
  can't, regardless of the compiler we use."
CompCert (had it been truly open source) would have provided that trustworthiness. And it can be ported to new architectures with the confidence that these ports won't silently break by random other changes.
link
mansr 4701 days ago
There are two fundamental problems with CompCert: 1) there is no formal, machine-readable specification of the C language, and 2) there is no formal, machine-readable specification of the target architectures. CompCert may be formally verified, but it's not necessarily a C compiler (even ignoring that it implements only a subset of C), nor does it necessarily compile for the advertised architecture.
link
qznc 4701 days ago
Addressing number 1) https://code.google.com/p/c-semantics/

Not perfect, but pretty good.

link
dmm 4702 days ago
""The CompCert verified compiler is distributed under the terms of the INRIA Non-Commercial License Agreement given below.""

It's some non-commercial non-free license. Only certain files are GPL? I don't think this would be redistributable...

link