Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Make formal verification and provably correct software practical and mainstream

github.com

Post reply on HN
Print view View original

91–100 of 203 posts

Re: Make formal verification and provably correct software practical and mainstream

#91

Post by namibj »

petergeoghegan wrote: post #75
guerrilla wrote: post #71

Earlier quoted context omitted.

> Serious question: do you really believe that? I mean it's a fact, so yes. You can prove programs are correct. The only possible flaw they can have is the specification is wrong. > The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people. That's very much not what I said. There may be many reasons. Assuming some conclusion without actual researc…

> You can prove programs are correct. The only possible flaw they can have is the specification is wrong. So specifications are kind of like programs? Have you heard of logical positivism? > That's very much not what I said. There may be many reasons. My point was that it always seems to be some external factor. That strikes me as being very convenient. > Assuming some conclusion without actual research is braindead.…

Well, seL4 has verifications of it's mixed-criticality hard-real-time guarantees (sufficiently tight bounds on scheduling latency (and such) to be useful) and data diode functionalities, and it's isolation properties have been verified not just at a fine-grained specification level but at a high-level human-readable level of invariant description. It doesn't cover timing and maybe some kinds of similar, other, side channels, but it's still extremely useful.

Formal verification shines in two situations: complicated optimized algorithms with a naive reference implementation you want to confirm equivalent, and high-level behavioral invariants of complex systems (like seL4's capability system, or a cluster database's consistency during literally all possible failover scenarios).

Re: Make formal verification and provably correct software practical and mainstream

#92

Post by practal »

guerrilla wrote: post #45
practal wrote: post #30

Earlier quoted context omitted.

I am sure we can do better than predicate logic or types, but the code needs to change also. Code should be more abstract and reusable. If possible, it should be a subset of the logic. There is no point in verifying the same stuff in JavaScript, Java, Rust, Swift, ... Furthermore, something that looks simple might need a lot of abstraction to become provable. Something might be simple to write down in code, but in or…

> First get mathematicians to actually like doing proofs with the help of a computer. Many are using type theoretic and HOL theorem proves already. What threshold do we need to reach? Isn't Lean HoTT? Isn't that pretty much good enough (modulo UI and tooling)? I ask the latter question because that was the original promise of HoTT but I haven't kept up to date on Lean, so I'm asking.

The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far.

A nice example is the recent formalisation in Lean of some ideas by Peter Scholze: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-...

That's great stuff, which shows what can in principle be done with this technology. But why is a team necessary to formalise Scholze's ideas? Note that Scholze himself doesn't touch Lean. In my opinion, the threshold is reached when Scholze himself sits down DURING the development of his ideas to interact with the proof assistant and develop+verify his ideas.

Re: Make formal verification and provably correct software practical and mainstream

#93

Post by muglug »

_vdpp wrote: post #32
muglug wrote: post #17

This builds on the success of Rust, but Rust has not been a success when it comes to [number of engineers writing professional code in the language]. By that measure it's still incredibly niche compared to interpreted languages. The main reason why formal verification has not had even the success of Rust is that most developers (myself included) don't know enough about the area to take an interest, and certainly don'…

Formal verification predates Rust by decades. The addition of lifetimes and the borrow checker are worthwhile contributions to the field of provably-safe software, but there are a lot of other soundness properties that Rust doesn’t check (though people are working on it).

I meant to say "this hopes to build on the success of Rust" — Rust is explicitly called out in the readme.

Re: Make formal verification and provably correct software practical and mainstream

#94

Post by guerrilla »

namibj wrote: post #91
petergeoghegan wrote: post #75

Earlier quoted context omitted.

> You can prove programs are correct. The only possible flaw they can have is the specification is wrong. So specifications are kind of like programs? Have you heard of logical positivism? > That's very much not what I said. There may be many reasons. My point was that it always seems to be some external factor. That strikes me as being very convenient. > Assuming some conclusion without actual research is braindead.…

Well, seL4 has verifications of it's mixed-criticality hard-real-time guarantees (sufficiently tight bounds on scheduling latency (and such) to be useful) and data diode functionalities, and it's isolation properties have been verified not just at a fine-grained specification level but at a high-level human-readable level of invariant description. It doesn't cover timing and maybe some kinds of similar, other, side c…

> with a naive reference implementation you want to confirm equivalent

I'm guessing you know this but in type theories like Agda you can just specify that the input and output to an algorithm has the desired properties, rather than needing to specify any reference algorithms. For example, you can just state that an implementation takes a list of X and that it outputs a sorted list of X. Nothing more is necessary in cases like that in such a system, no code, just the single type.

Re: Make formal verification and provably correct software practical and mainstream

#95

Post by tgv »

digitalice wrote: post #46

Been following the development of Dafny: https://www.microsoft.com/en-us/research/project/dafny-a-lan...

Looks interesting, perhaps because it seems to be a bit more down to earth than some of the other proposals where you have to derive Whitehead&Russell before you're allowed to use the + operator. But it also seems quite dead. The latest link is from 2012.

Re: Make formal verification and provably correct software practical and mainstream

#96

Post by namibj »

guerrilla wrote: post #94
namibj wrote: post #91

Earlier quoted context omitted.

Well, seL4 has verifications of it's mixed-criticality hard-real-time guarantees (sufficiently tight bounds on scheduling latency (and such) to be useful) and data diode functionalities, and it's isolation properties have been verified not just at a fine-grained specification level but at a high-level human-readable level of invariant description. It doesn't cover timing and maybe some kinds of similar, other, side c…

> with a naive reference implementation you want to confirm equivalent I'm guessing you know this but in type theories like Agda you can just specify that the input and output to an algorithm has the desired properties, rather than needing to specify any reference algorithms. For example, you can just state that an implementation takes a list of X and that it outputs a sorted list of X. Nothing more is necessary in c…

Well, yes, that falls under the second case: behavioral invariants of complex systems.

And the reference for "sorting" could likely be a deterministic bogosort and certainly a primitive bubblesort.

Even if you're just looking at sorting stability, you're past what your simple "sorted" type would cover.

Most things are far less trivial than "sorted list", including (almost?) all interesting practical applications of formal verification in the life of a "normal" software engineer.

Re: Make formal verification and provably correct software practical and mainstream

#98

Post by kaba0 »

_vdpp wrote: post #66
Hizonner wrote: post #64

Earlier quoted context omitted.

I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are…

A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove termination,” and like you said most of the useful programs we write can be shown to terminate just fine.

You forget about Rice’s theorem. Termination is not that exciting, but the existence of race conditions and a million other properties are - and those are not possible to prove true in general.

Re: Make formal verification and provably correct software practical and mainstream

#99

Post by kaba0 »

marcosdumay wrote: post #23
daenz wrote: post #6

Outside of mission critical applications, if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.

We use static type systems all the time, as well as specialized checkers and linters, and none of those showed themselves to have "costs greater than the cost of the bugs". And none of them are even nearly similar to "demanding your house have all perfect right angles and completely level surfaces". Do you have any reason to believe that all the rest of the verification theory is completely impractical when every pie…

> Do you have any reason to believe that all the rest of the verification theory is completely impractical when every piece that was packaged in a usable context became a hit?

While I am by no means have enough knowledge to claim such, but let’s just add that ordinary types are a so-called “trivial property”. Many, actually interesting properties can’t be proved as per Rice’s theorem in every case.

Re: Make formal verification and provably correct software practical and mainstream

#100

Post by ebingdom »

Hizonner wrote: post #64
AlotOfReading wrote: post #31

I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible. Important questions like how you implement the design pillars without running smack into the i…

I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are…

> However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are undecidable in general. Rice's theorem, blah, blah, blah. For any given property and any given language, I can show you a program in that language such that you cannot determine whether that program has that property.

Decidability has nothing to do with this kind of formal verification. The tool doesn't have to decide the correctness of a program. The tool merely needs to check the validity of a proof of the program's correctness, which is rather trivial. Coming up with the proof is the hard part, and that responsibility still falls mostly on humans.

Post reply on HN