Hacker News Reader

Comment by akomtu | Hacker News Reader

I suspect that verifying software is a lot like the termination problem of Turing machines: the more useful properties you want to verify, the closer it is to NP completeness. So a practical verifier should limit its scope to a modest subset of software and settle on verifying sonething with a sufficient degree of confidence, which is lower than 100%.

View on HN

It turns out that you can write proven correct C compilers (CompCert), proven correct Operating Systems (seL4), and proven correct secure network protocols using proof assistants like Coq and F*. All of those proof assistants are using languages that are not Turing complete. You have to prove termination if the proof assistants can’t automatically prove it. So being Turing complete is not really necessary for writing complex software.

Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-is-undecidable-to-pr...

Both termination and verification go beyond NP completess, in that they are undecidable. Also, "verifying so[m]ething with... confidence... lower than 100%" is known as testing.

Termination is undecidable in general but that is not a problem in practice. Proof assistants like Coq, LEAN etc. can automatically prove termination for most practical code. And if not, the developer has to prove termination by hand. Which is not hard in most cases I have encountered. And if you still can’t do it you simply add a “fuel” natural number counter that guarantees termination (exit when out of fuel).

Reply on news.ycombinator.com