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

111–120 of 203 posts

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

#111

Post by csande17 »

lelanthran wrote: post #105
johnbender wrote: post #29

Earlier quoted context omitted.

I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.

> I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. If that was at all achievable, we'd have a compiler that took the "specification in a formal language/logic" and emitted native code/applications/programs. We'd then call the "specification in a formal language/logic" a programming language. Sure, there are a lot of formal languages f…

If you're writing a sorting algorithm or a hash table implementation or something, then the spec is meaningfully different from the code. The spec says "the output array is sorted", the program describes some particular strategy for sorting it, and then you use the proof tools to make sure that the strategy actually works to sort the array in all cases.

But for things like UI code, I too am having trouble imagining a spec that is concrete enough to be useful for formal verification and does not have some trivial 1:1 correspondence to the implementation. (If anyone knows of an example, I'd really be interested in seeing it!)

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

#112

Post by ebingdom »

kaba0 wrote: post #107
ebingdom wrote: post #104

Earlier quoted context omitted.

That's not what Rice's theorem states. Rice's theorem states that interesting properties are undecidable, not that they can't be proven. Undecidability is not relevant when you are providing the proofs to the computer.

If you would have a proof, you could make an algorithm that verifies it, making it decidable, couldn’t you?

Checking proofs is decidable. Coming up with proofs is undecidable.

This tool does the former, leaving the latter up to humans.

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

#113

Post by ebingdom »

kaba0 wrote: post #98
_vdpp wrote: post #66

Earlier quoted context omitted.

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.

No, docandrew is correct. You are incorrectly applying Rice's theorem.

Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "magmide" tool doesn't claim to do that. It merely checks proofs that have already been found (e.g., by a human), which is trivially decidable.

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

#114

Post by ebingdom »

practal wrote: post #92
guerrilla wrote: post #45

Earlier quoted context omitted.

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

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

The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.

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

#115

Post by porcoda »

daenz wrote: post #14
guerrilla wrote: post #12

Earlier quoted context omitted.

> if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. It may already be. Where's the research? It may not be happening just because of quarterly cycles, other misaligned incentives, culture or all kinds of other reasons. > Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and comp…

>Software often doesn't. And yet the world keeps turning, tech companies keep profiting, and customers are generally happy with the value provided, all without formally provable code bases. How does "provably correct" improve on this without extending timelines and costing more?

> customers are generally happy with the value provided

Don't confuse resignation and ignorance with happiness. People are used to computer systems just breaking and being the root of various problems (e.g., identity theft, privacy leaks, systems that just don't work some days for no apparent reason, and so on). The fact that they accept this flaky and unreliable state as the status quo doesn't mean they're happy with it - they just don't understand that better is actually possible.

I work in the security and assurance world. The biggest obstacle we face isn't technical - it's social. Developers want the route of least effort and least time to get products to market, and end users are largely ignorant of the fact that the world doesn't have to be full of garbage software. At this point, I'm rooting for a massive change in the legal landscape to start treating software defects the way we do engineering defects in physical systems. Developers and businesses aren't going to do the right thing by choice, so a giant hammer in the form of the legal system is likely to be the only thing to force change. I am fully aware of the consequences of that (e.g., it will likely severely chill open source, and will likely slow many business sectors down) - and I accept this. I'd take those consequences for the safety/security/assurance outcomes, even if they cause havoc on the revenue/business side and make "10x" python hackers grumpy. People will likely take formal assurance methods more seriously when there are actual consequences to deploying unsafe/insecure systems.

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

#116

Post by lelanthran »

csande17 wrote: post #111
lelanthran wrote: post #105

Earlier quoted context omitted.

> I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. If that was at all achievable, we'd have a compiler that took the "specification in a formal language/logic" and emitted native code/applications/programs. We'd then call the "specification in a formal language/logic" a programming language. Sure, there are a lot of formal languages f…

If you're writing a sorting algorithm or a hash table implementation or something, then the spec is meaningfully different from the code. The spec says "the output array is sorted", the program describes some particular strategy for sorting it, and then you use the proof tools to make sure that the strategy actually works to sort the array in all cases. But for things like UI code, I too am having trouble imagining a…

> If you're writing a sorting algorithm or a hash table implementation or something, then the spec is meaningfully different from the code. The spec says "the output array is sorted", the program describes some particular strategy for sorting it, and then you use the proof tools to make sure that the strategy actually works to sort the array in all cases.

I dunno. Thinking more deeply about the specification for a sorting algorithm, it makes sense that the specification includes the O(n) runtime (or memory usage, or both), or else it's an informal specification.

If the spec is really nailed down formally then the specification language really would be the implementation language too.

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

#117

Post by [deleted] »

ebingdom wrote: post #114
practal wrote: post #92

Earlier quoted context omitted.

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…

> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.

[deleted]

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

#118

Post by practal »

ebingdom wrote: post #114
practal wrote: post #92

Earlier quoted context omitted.

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…

> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.

Not if you do software the right way. Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ...

Furthermore, I don't think cutting-edge math needs a much different approach from cutting-edge software. You need to be able to express your thoughts succinctly, and have the tools to reason about them.

It is often said that software verification is different because there is much more to verify, but on a more shallow level. I instead think software is just not done at the right level of abstraction.

Software is at the same time more and less than math. More, because in addition to understanding a topic, you also need an implementation, which has additional issues like speed and memory usage, battery life, etc. Less, because if you do a nice implementation, nobody is asking about its correctness, or how well you understood the topic in the first place. For software today, a nice implementation is much more important than a correctness proof.

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

#119

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.

There was a version of Lean that supported HoTT, and I think it helped in making Lean popular. But that support has been dropped in Lean 3, and Lean 4 does not support it either. Lean 4 itself seems to be a radical rewrite, and libraries written for Lean 3 do not work in Lean 4.

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

#120

Post by [deleted] »

ebingdom wrote: post #113
kaba0 wrote: post #98

Earlier quoted context omitted.

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.

No, docandrew is correct. You are incorrectly applying Rice's theorem. Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "magmide" tool doesn't claim to do that. It merely checks proofs that have already been found (e.g., by a human), which is trivially decidable.

[deleted]
Post reply on HN