News for hackers. Stuff that matters.

A comment on Make formal verification and provably correct software practical and mainstream.

Re:Make formal verification and provably correct software pr... by akomtu on Saturday May 28, 2022 @09:01PM (#31545242)
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%.
[ Parent | on HN ]
Re:Make formal verification and provably correct software pr... by mbrodersen on Sunday May 29, 2022 @10:07PM (#31554844)
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.
[ Parent | on HN ]
Re:Make formal verification and provably correct software pr... by blainehansen on Saturday June 04, 2022 @12:50AM (#31617107)
Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-is-undecidable-to-pr...
[ Parent | on HN ]
Re:Make formal verification and provably correct software pr... by warkdarrior on Saturday May 28, 2022 @09:47PM (#31545502)
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.
[ Parent | on HN ]
Re:Make formal verification and provably correct software pr... by mbrodersen on Sunday May 29, 2022 @10:12PM (#31554870)
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).
[ Parent | on HN ]