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 t

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.