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

51–60 of 203 posts

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

#51

Post by AnimalMuppet »

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…

This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Those provide formal verification of some aspects of the code. And that's great! It's progress!

Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation that "it's amazing how many bugs there can be in a formally verified program" is no longer true.)

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

#52

Post by AnimalMuppet »

hn_urbit_thr123 wrote: post #43

Is it even realistic to make a provably secure/stable applications on an OS like windows or linux? This (provable correctness of programs, at the expense of performance) is one of the explicit design goals or urbit. I know HN hates urbit and don't want to rehash that, but it seems like a good goal for some use cases and I'm not sure it's possible to achieve without building the OS around it.

Let's say that Urbit claims to be formally, provably secure. But approximately nobody actually understands Urbit, which means that nobody knows whether the proof is solid. So as an outsider, I have to either take it on faith that it's secure, or I have to spend a fair amount of time immersing myself in this hard-to-learn system to see if the claimed benefits are really there.

But it's not just Urbit. Rust has essentially the same problem.

In fact, perhaps all of formal verification has this kind of problem. How do you prove the benefits to someone who doesn't know the tools?

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

#53

Post by akomtu »

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

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

#54

Post by mjb »

Cloudef wrote: post #47

Do we have formal verification for formal verification yet? I want to make sure my verification does not have bugs.

Yes, it's an active area of research. One very recent example, focusing on Dafny: https://www.amazon.science/publications/testing-dafny-experi...

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

#55

Post by marcosdumay »

AnimalMuppet wrote: post #51
marcosdumay wrote: post #23

Earlier quoted context omitted.

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…

This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Those provide formal verification of some aspects of the code. And that's great! It's progress! Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation…

Well, the article has quite a list of "some aspects" of your code the author is working on.

I have no reason why any of them could not be successful. I don't expect all of them to be, but anyone that gets there is already a huge advance.

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

#56

Post by 8note »

guerrilla wrote: post #44
daenz wrote: post #39

Earlier quoted context omitted.

>Ever heard of this thing called ransomware, for example? Identity theft? Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. >Obviously the answer is that they could profit more and be happier. Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You…

> Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. > Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear th…

It's a tradeoff though - you could spend the time looking for bugs between the design and implementation, or you could get the implementation out sooner and get feedback and iterations on the design

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

#57

Post by Transfinity »

er4hn wrote: post #25
csande17 wrote: post #21

As the article mentions, formal verification techniques are primarily used today for two things: - Creating secure "core" code -- library functions and kernels and stuff, where the things they're supposed to do are very well-defined. - Verifying specific, narrowly defined properties, like how Rust's borrow checker guarantees that your program doesn't try to write to the same value from two different threads at once.…

I would love to see a fuzzer applied to business logic. It should take design requests from PMs and execucritters and ask pointed questions about edge cases.

I love this idea. I bet you could get surprisingly useful results just using a language model like GPT-3.

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

#58

Post by agentultra »

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…

It is wishful thinking. Iris is cool and all but extracting useful programs from proofs is still an open research area. I don’t want to discourage someone from trying but it would help to be pragmatic.

At least the author seems somewhat aware of this when they describe the repo as a collection of earnings and ravings.

I’ve been interested in this since 2015 or so and even then the cost of doing formal verification had come down a lot. It has continued the downward trend. But we are still a long way from a language that industry programmers can use to write proofs and extract programs from.

One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.

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

#59

Post by markisus »

I think there is a project quite similar to this one called Verifiable Software Toolchain (VST) in which you can write a C program, convert it into a massive Coq expression, and then write theorems about that expression in Coq. The Software Foundations series has a volume about it [1], which I found to be an order of magnitude harder to understand than the other volumes.

It feels like the magmide project aims to the same goal as VST. It's unclear how it will improve on what VST has done. It may just be that formal verification of real world languages is inherently complex.

[1] https://softwarefoundations.cis.upenn.edu/vc-current/index.h...

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

#60

Post by petergeoghegan »

AnimalMuppet wrote: post #50
_vdpp wrote: post #37

Earlier quoted context omitted.

I think the cost of provably correct software is actually much lower, but you pay more of it up front. The perceived incentives of being first to market are higher than that of quality software. I suspect eventually there will be a big lawsuit where the blame can be laid on negligence in the software development and the incentives might change somewhat.

The first such successful lawsuit is going to change the landscape. Not just "somewhat" - it's going to be a massive change.

This sounds like motivated reasoning to me. Have you heard of Therac-25?

You might be inclined to suggest that that could have been prevented if only they'd used formal methods. Perhaps that's true. It's something that could have been prevented in many different ways, though. Yet it still happened.

Post reply on HN