|
|
|
|
|
|
by jroesch
3270 days ago
|
|
|
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. |
|
|