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

101–110 of 203 posts

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

#101

Post by ebingdom »

Animats wrote: post #20

"And all existing proof languages are hopelessly mired in the obtuse and unapproachable fog of research debt created by the culture of academia." Yes. As I wrote 40 years ago: "There has been a certain mystique associated with verification. Verification is often viewed as either an academic curiosity or as a subject incomprehensible by mere programmers. It is neither. Verification is not easy, but then, neither is wr…

I was with you until:

> 5) Too much gratuitous abstraction. The old version was "everything is predicate calculus". The new version is "everything is a type" and "everything is functional".

Total functional programming with types is literally the same as writing proofs in intuitionistic logic, in a technical sense (the Curry Howard correspondence). This isn't a new fad. It's a deep result that was known more than half a century ago.

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

#102

Post by ebingdom »

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.

> Isn't Lean HoTT?

No. Lean is good old fashioned Martin-Löf type theory. HoTT is that type theory + univalence + higher inductive types. Lean actually has proof irrelevance, which is incompatible with HoTT.

But the good news is you don't need HoTT to verify software. Type theory is already quite capable of it, despite what others in this thread would like you to believe.

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

#103

Post by hath995 »

tgv wrote: post #95
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.

It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny

I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I learned in college rather than the weird magic keywords of Coq.

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

#104

Post by ebingdom »

kaba0 wrote: post #99
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…

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

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.

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

#105

Post by lelanthran »

johnbender wrote: post #29
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 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 for specifying logic with checkers that ensure no bugs in the input specification exist, but AFAIK none of them are useful enough to emit programs.

Needing a human to translate one formal language (the formal spec) into another formal language is pointless and useless, because then the human may as well just translate human language specification into formal language.

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

#107

Post by kaba0 »

ebingdom wrote: post #104
kaba0 wrote: post #99

Earlier quoted context omitted.

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

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?

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

#108

Post by lelanthran »

_vdpp wrote: post #37
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.

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 perceived incentives of being first to market are higher than that of quality software.

"Perceived"?

It's very rare that shipping later because of $quality-concerns is profitable. In most cases, that "later" never arrives anyway.

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

#109

Post by lelanthran »

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.

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

I'd argue that, if there was going to be a needle-mover lawsuit, it would have happened by now. Until there is evidence that it will happen, we can continue assuming that it won't.

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

#110

Post by chmod600 »

shoo wrote: post #18
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.

Exactly. In many settings it is quite a reasonable business decision to regard a bug as WONTFIX. Here's one example: developer: adding proposed feature A to API B may result in displaying inconsistent data to the customer, in this kind of situation team owning service of API B, some weeks later: thank you for flagging that. we have thought about this, and propose a slightly different API design B'. let's meet to disc…

Defects, and potential defects, tend to cause a background of mental overhead, and communication overhead, throughout the organization. People have to remember what kinds of assumptions are broken under what circumstances, and relate that to a business impact.

There's a mental unburdening when you can just say "situation X won't happen".

Post reply on HN