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

11–20 of 203 posts

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

#11

Post by daenz »

KSteffensen wrote: post #8
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.

Why does it always have to be all or nothing? Is your codebase 100% covered by unit tests? You don't have to make sure all the angles of your house are perfect right angles, but there's probably a couple that really have to be. Formally verify those and live with manageable imperfection for the rest.

"All or nothing" is not the point I'm making, it's "any or nothing." Unittests frequently have justifiable value for their effort, even when only providing partial coverage. I'm arguing that the effort involved in creating formal proofs for any part of your software is almost never worth the benefits, outside of mission critical applications, when a dozen simple unittests could provide 99.99% confidence. And certainly not worth it enough to become "mainstream", which is the title of the post.

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

#12

Post by guerrilla »

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.

> 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 completely level surfaces. Living with manageable imperfection is far more realistic.

The difference is that those things are all within tolerances and serve their purposes and function correctly. Software often doesn't.

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

#14

Post by daenz »

guerrilla wrote: post #12
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.

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

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

#15

Post by michaelsbradley »

naniwaduni wrote: post #4
eurasiantiger wrote: post #3

Can we formally verify the software cannot be used for evil?

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

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

#16

Post by toast0 »

Formal verification needs machine readible formal specifications, but any kind of written specification, informal or not was pretty hard to find in my career at internet giants. Maybe you can get a formal spec in aerospace or FDA regulated implanted devices, but cost to write the spec, let alone to follow the spec is way too high when the spec needs to change at the whim of a hat.

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

#17

Post by muglug »

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't know enough about the area to pursuade skeptical managers.

Unless a big company comes forward with a bunch of case studies about how they used formal verification successfully I can't see the developer mindset changing.

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

#18

Post by shoo »

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

product owner: the scenario that would trigger that situation requires a combination of unusual events: it has to coincide with a scheduled batch process, and the customer would need have unusual characteristics that are rather different from the distribution we observe. When the defect happens, the impact to the customer and our business is not so bad.

developer: That's fair. given how the feature works there are many other ways it can show inaccurate data to the customer as well.

engineering manager: how about we don't fix it, does anyone disagree?

everyone agrees not to fix it

A more interesting question is to ask "in which business situations does it make sense for formal verification to be used?". If you want to get paid to play with formal verification in the day job, you'd best find a business context where it is business critical to identify and remove design and implementation defects early, and it is worth spending a lot of money trying complementary techniques for doing so.

For my above example:

- the defect is not related to a core capability of the product. if it occurs, the defect does not cause a huge impact to the customer or the business. it may mildly annoy the customer.

- how the feature works is fairly ill-defined anyway, there are many things that influence it, and it's job isn't to preserve customer data, so data integrity isn't a huge priority

- if the defect did start causing substantial problems in future, it would be possible to change this decision and decide to fix it. the cost of fixing it later might be 5x fixing it now, but it wouldn't e.g. require a product recall or risk bankrupting the company.

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

#19

Post by 88913527 »

For functional stuff, sure, but I don't think this is achievable within the UI domain. CSS rules have implementation details that change how you write it (some problems have workarounds), for example there's a documented set of issues in flex implementations maintained here: https://github.com/philipwalton/flexbugs

It might be practical and possible to become mainstream for some domains, but it's doubtful for others. The most practical solution for UI is visual regression testing across browsers.

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

#20

Post by Animats »

"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 writing reliable computer programs. More than anything else, verifying a program requires that one have a very clear understanding of the program’s desired behavior. It is not verification that is hard to understand; verification is fundamentally simple. It is really understanding programs that can be hard."[1]

What typically goes wrong is one or more of the following:

1) The verification statements are in a totally different syntax than the code.

2) The verification statements are in different files than the code.

3) The basic syntax and semantics of the verification statements are not checked by the regular compiler. In too many systems, it's a comment to the compiler.

4) The verification toolchain and compile toolchain are completely separate.

None of this is theory. It's all tooling and ergonomics.

Then, there's

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

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

Post reply on HN