Hacker News Reader

Comment by throw10920 | Hacker News Reader

Assuming it's possible for most proofs to become automatically generated (which I don't think is a given), then it seems like verification work will shift from manually writing proofs into writing the specification from which proofs will automatically be generated - in which case, verification engineers will be able to look forward to an exciting future of figuring out how to tell the computer what is meant by "is".

Or doing system implementation directly - it doesn't seem like automated program synthesis is going anywhere fast...

(I jest, while still growing to be more of a fan of type systems, borrow checkers, and formal proofs)

View on HN

I mean that's always been the key skill of programming. Telling the computer how to do the thing isn't the hard part, figuring out exactly what needs to be done is.

More likely we’re looking at codesign/correct-by-construction for fully general purpose verification.

In many cases it’s possibly to refine a state machine based specification to an imperative implementation (and thereby carry safety properties down to the implementation) but at present the implementation usually looks like the state machine (thus codesign)

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.

> 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.

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.

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.

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.

Reply on news.ycombinator.com