Hacker News new | ask | show | jobs
by ncmncm 1696 days ago
A proof about a state machine is more useful than a proof about a program, or an automatically generated program. Proving that a program correctly implements a state machine is a much simpler exercise than teaching a proof system about your programming language.
1 comments
Jweb_Guru 1696 days ago
> A proof about a state machine is more useful than a proof about a program, or an automatically generated program.

Easier maybe, but more useful? I disagree. Just because it's difficult to prove things about real programs doesn't change the fact that a formally verified program has really important advantages--like being able to actually run it, and knowing the executing code actually fulfills the spec rather than relying on a human translation layer.

link
ncmncm 1695 days ago
No, more useful. A proof about a state machine applies to any implementation of the state machine, in any language. A generated program is only itself. Any needed modifications make it not the program generated, or proven.

Furthermore: such output depends, for correctness, on a complete and accurate description of the salient details of the programming language, and the environment it needs to run in, provided to the proof system. But such a description is more complicated and error-prone than the description of the state machine. So, you need an extra proof that the language and system description are accurate and complete, which is not provided.

link
Jweb_Guru 1695 days ago
A proof that the language and system description are accurate and complete is very difficult, I agree. But it only has to be done once, it does not have to be repeated for each proof, so that does not seem relevant to me wrt the advantages of such a proof.

As for your first point, I would wager (having done it many times) that it is considerably easier to translate a proven, working program to another language correctly, than it is to do the same thing with an abstract state machine.

link
ncmncm 1695 days ago
For it to be "done once", it has to be done at all. I have not seen any reason to believe it was done at all. When posting a boast about having done the easy part, it does not inspire confidence that the hard part was done, too, but nobody thought the hard part was worth mentioning.

So, until I see the announcement, the reasonable interpretation is that it has not been done.

link