[sigstoat]

i agree that miod isn't talking about proofs. but i don't think adultSwim was making that claim, either.

> The only way to prove code correct is by reference to some kind of specification.

there are other interesting properties to prove besides "correctness of the entire compiler".

you could prove the entire compiler version n+1 emits the same code as version n, modulo $bugfix.

you could prove that individual optimizations are, on their own, correct with regards to the AST or IR that gcc operates on.

neither of those require a formalized spec of C. the first would probably make miod pretty happy. sadly one isn't going to get gcc man handled into a proof assistant, ever.

[fusiongyro]

Those are interesting and extremely good ideas, thanks for pointing them out.

I do wonder if OpenBSD would accept a C compiler built on a small functional language amenable to these kinds of proofs. I suppose fulfilling the portability requirements is priority one, then stability. I just wonder if they would accept something not written in C at all.