Hacker News Reader

Comment by adrianN | Hacker News Reader

We suck really hard at proving code correct that was written explicitly with the goal in mind to be formally verified. The techniques there are still quite immature. I wonder how long it will take until we have a reasonably working pipeline of ML+formal verification. Maybe it's just easier to generate correct code from the spec than to learn it from examples and then verifying it with the specification?

View on HN

"We suck really hard at proving code correct that was written explicitly with the goal in mind to be formally verified."

That is why I am not a huge fan of proving code in the first place. If you have a really complicated proof of formal correctness, then who guarantees you, there is no misstake in the proof itself? At least this is what I have seen in university, lots of complicated stuff on the whiteboard, with a result. And then someone figured out, it was wrong.

So I rather do lots of testing, for all known test cases.

Your automatic proof checker guarantees that there is no mistake in the proof. That's the easy part! The real question is who guarantees that your specification is what you actually want?

Automatic proof checkers still have bugs in them. However, one nice characteristic is that, since its algorithms are so general, i.e. about the language rather than about the problem you're solving (e.g. sorting), any bugs in the checker are either so common they hit every problem solution and are easily discovered and fixed, or so rare that it affects no real-world problem solutions.

The kernel of an automatic proof checker is much easier to test and verify than the programs you verify using a proof checker though.

+1 verification tends to be the easy part.

Sure, not all bugs are kernel bugs though.

> So I rather do lots of testing, for all known test cases.

How is this any different? You can still make mistakes in your test code, test data, omit cases that would fail, etc. I think I'd be less confident in a set of unit tests than I would with an automated proof checker.

Tests are simple to unterstand.

Complicated proofs I do not understand, without much effort.

And I surely know that you can make mistakes with test cases as well. So I surely do not claim my way to be superior. But it works way better for me.

Test cases are not necessarily simple to understand.

Especially the test cases needed to trigger some deep bug.

And so aphyr gets paid, for instance. You may not even be able realistically to run a test case. The laws of life say your 10000 core compute job will fail non-deterministically only after a day or so. It would clearly be helpful to have at least some formal guarantees, such as liveness at some level.

Reply on news.ycombinator.com