[fusiongyro]

I don't think that's the message here at all. The only way to prove code correct is by reference to some kind of specification. If that spec is a standard full of implementation-defined behavior (and worse, contradicted in practice by all the other vendors) a correctness proof is not really going to convey what it sounds like it would.

What Miod is really asking for is an open source compiler that puts stability and portability over compiler optimization. If it weren't for optimizations and the endless fiddling that goes with them, gcc would have remained stable. It is already the only option that meets their portability requirements.

[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.