Neural programmer better than Quicksort

Re:Neural programmer better than Quicksort by adrianN on Friday July 10, 2020 @03:20AM (#23789022)

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?

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by hutzlibu on Friday July 10, 2020 @04:34AM (#23789400)

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

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by adrianN on Friday July 10, 2020 @04:59AM (#23789523)

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?

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by infinity0 on Friday July 10, 2020 @05:48AM (#23789752)

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.

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by adrianN on Friday July 10, 2020 @05:53AM (#23789776)

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

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by chrisandchips on Friday July 10, 2020 @06:49AM (#23790125)

+1 verification tends to be the easy part.

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by infinity0 on Friday July 10, 2020 @10:29AM (#23791776)

Sure, not all bugs are kernel bugs though.

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by louthy on Friday July 10, 2020 @06:07AM (#23789857)

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

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by hutzlibu on Friday July 10, 2020 @06:29AM (#23789983)

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.

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by eru on Friday July 10, 2020 @09:39AM (#23791346)

Test cases are not necessarily simple to understand.

Especially the test cases needed to trigger some deep bug.

[ Parent | on HN ]

Re:Neural programmer better than Quicksort by gnufx on Friday July 10, 2020 @04:13PM (#23795900)

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.

[ Parent | on HN ]