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

21–30 of 203 posts

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

#21

Post by csande17 »

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'm not sure formal techniques will be as useful when expanded to other areas. Most of the bugs I encounter day-to-day happen because the programmer had the wrong goal in mind -- if you asked them to create a formal proof that their code worked, they would be able to do that, but it would be a proof that their function did a thing which was not actually the thing we wanted. (Similarly to, e.g., unit tests that do not actually test anything because they're just line-by-line reproductions of the original code but with every function call mocked out.)

Has anyone successfully applied proof techniques to reduce defects in UI development, "business logic", or similarly fuzzy disciplines?

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

#22

Post by yourapostasy »

> ...existing uses of Iris perform the proofs "on the side" using transcribed syntax tree versions of the target code rather than directly reading the original source.

I'm a formal verification dummy, so can someone please confirm if this means these uses of Iris are creating an Abstract Syntax Tree (AST) of the source, then operating upon that AST?

If so, can I please get an ELI5 why there is a salient formal verification outcomes difference between using the AST and "directly reading the original source"?

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

#23

Post by marcosdumay »

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 piece that was packaged in a usable context became a hit?

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

#24

Post by guerrilla »

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?

> tech companies keep profiting, and customers are generally happy with the value provided

Obviously the answer is that they could profit more and be happier.

Ever heard of this thing called ransomware, for example? Identity theft? And you must know, this stuff is only the beginning... Just wait until the day everyone's private Facebook chats are available on torrent.

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

#25

Post by er4hn »

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.

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

#26

Post by moeris »

michaelsbradley wrote: post #15
naniwaduni wrote: post #4

Earlier quoted context omitted.

gonna have to formally define evil

Evil: the privation of a good that should be present. It is the lack of a good that essentially belongs to a nature; the absence of a good that is natural and due to a being. Evil is therefore the absence of what ought to be there. https://www.catholicculture.org/culture/library/dictionary/i... https://en.m.wikisource.org/wiki/Catholic_Encyclopedia_(1913...

No post body was provided.

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

#27

Post by practal »

homodeus wrote: post #10
pid-1 wrote: post #2

I've started watching Lamport's TLA+ course in YT and it totally blew my mind. What are other good resources in formal verification?

The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/

If you are more practical than religious, try this: https://functional-algorithms-verified.org

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

#28

Post by [deleted] »

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

[deleted]

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

#29

Post by johnbender »

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.

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

#30

Post by practal »

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 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 order to come up with a notion of correctness for it, and actually prove it, might require something significantly more complicated.

Infatuation with Hoare-Logic is part of the problem (that's what the paper you link uses, I think?). Thinking that verifying programs is easier than doing proper math on the computer is a dead end. First get mathematicians to actually like doing proofs with the help of a computer. THEN you might have a chance of tackling more practical applications like program verification without using an insane amount of resources.

Post reply on HN