Hacker News Reader

Comment by Scea91 | Hacker News Reader

> your specification is simply "an optimized program always behaves the same as the original"

I wouldn't say it is simple, since it is undecidable for general programs.

Daniel's point is that the specification itself is simple, he is saying nothing about the complexity of proving that your program matches the specification.

The decidability of the specification isn't important in this context. It is known there is no procedure to build a proof of this specification for any language or optimization, but as humans we can prove that it holds for a specific configuration of compilers, and optimizations, and have done so many times, for example CompCert, Alive, etc.

The specification is simple in the sense that it is easy to understand what it states and to confirm that it has the intended meaning. This does not mean that all proofs of the specification will be simple, but once you do construct a machine-checkable proof of the specification, your level of confidence that the system is correct will be extremely high (commensurate to the simplicity of the specification) and will not depend on the complexity of the proof.

The point is that the specification is short and human understandable: you get confidence that bugs are unlikely to exist in the specification. Now if you also can prove that your optimization passes fulfill the specification you've obviously gained a lot of value. It doesn't matter that deciding the correctness of arbitrary program transformations is undecidable if you happen to succeed in proving that the ones actually implemented are correct.

Reply on news.ycombinator.com