3 ms·

> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result This is obvious for

> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input. Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.

deterministic 2mo ago
The trick is to start with the smallest possible implementation of a spec and proving it correct. You then add a more advanced and faster implementation and prove that the 2nd implementation implements the 1st. Etc. etc. It's called refinement and it's a great way to prove really complex software correct. You basically have a formally proven correct chain of software from simple to advanced. CompCert is an example of how to do this.