4 ms·
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
by pdw 13y 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.
- mansr 13y agoThere 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.
- qznc 13y agoAddressing number 1) https://code.google.com/p/c-semantics/ https://code.google.com/p/c-semantics/ Not perfect, but pretty good.