[HN Gopher] Make formal verification and provably correct softwa...
___________________________________________________________________
Make formal verification and provably correct software practical
and mainstream
Author : peanutcrisis
Score : 31 points
Date : 2022-05-28 21:17 UTC (1 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| daenz wrote:
| 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.
| marcosdumay wrote:
| 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?
| KSteffensen wrote:
| 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.
| daenz wrote:
| "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.
| guerrilla wrote:
| > 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.
| daenz wrote:
| >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?
| guerrilla wrote:
| 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.
| shoo wrote:
| 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 <details>
|
| 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.
| Buttons840 wrote:
| I applaud the research. Of course, those organizations creating
| and suffering from the most bugs will be the least able to
| utilize such a language.
| pid-1 wrote:
| I've started watching Lamport's TLA+ course in YT and it totally
| blew my mind.
|
| What are other good resources in formal verification?
| dqpb wrote:
| State Machines are the natural paradigm in TLA+. OOP is just
| poorly organized state machines. Try rewriting an OO program
| with state machines and you'll have something that directly
| maps to TLA+, and it should demystify much of formal
| verification.
| homodeus wrote:
| The Bible of formal software logic, free of charge:
| https://softwarefoundations.cis.upenn.edu/
| toast0 wrote:
| 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.
| muglug wrote:
| 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.
| eurasiantiger wrote:
| Can we formally verify the software cannot be used for evil?
| naniwaduni wrote:
| gonna have to formally define evil
| sharkbot wrote:
| The constructivist in me thinks we could define it
| inductively :)
| michaelsbradley wrote:
| 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.
| ..
| Bjartr wrote:
| Sure, given a formal definition of evil.
| 88913527 wrote:
| 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.
| Animats wrote:
| _" 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
| csande17 wrote:
| 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?
| yourapostasy wrote:
| _> ...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"?
___________________________________________________________________
(page generated 2022-05-28 23:00 UTC)