5 ms·

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 wil

by daenz 4y ago

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.

KSteffensen 4y ago
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 4y ago
  "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 4y ago
> 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 4y ago
  >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 4y ago
    > 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.
    - deleted 4y ago
      [deleted]
    - daenz 4y ago
      >Ever heard of this thing called ransomware, for example? Identity theft? Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. >Obviously the answer is that they could profit more and be happier. Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly?
      - guerrilla 4y ago
        > Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. > Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly? The revenue could come from savings on fixing bugs, paying for ransomed assets and all other costs that come from bugs. You're just assuming that doesn't add up and that there's no other reason that we don't do formal verification. That's just stupid. Show me the studies. Your claim is just as strong as the claim you think I'm making, but you missed my point entirely.
shoo 4y ago
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.
- chmod600 4y ago
  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".
  - 4y ago
marcosdumay 4y ago
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?
- AnimalMuppet 4y ago
  This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Those provide formal verification of some aspects of the code. And that's great! It's progress! Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation that "it's amazing how many bugs there can be in a formally verified program" is no longer true.)
  - marcosdumay 4y ago
    Well, the article has quite a list of "some aspects" of your code the author is working on. I have no reason why any of them could not be successful. I don't expect all of them to be, but anyone that gets there is already a huge advance.
  - topspin 4y ago
    > This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Yes indeed. That is insightful. Is there a name for this process?
    - AnimalMuppet 4y ago
      Well, in AI, the process is called "AI can never succeed". So maybe the general thing is "X can never succeed", where X is some hugely ambitious (and ambiguous) thing, like "AI" or "formal software verification" or "curing cancer". We're probably never going to cure cancer - that is, have some treatment that conquers all cancers. Instead, we get "for this specific type of cancer, for these specific conditions, this treatment has a higher survival rate than the ones we had before". Over time, that adds up to a lot of people living out their days rather than dying early. And maybe software verification is the same. Enough ways of verifying specific aspects of software, and bugs have fewer places to hide. It won't find all bugs, but we'll still get better software. But "X can never succeed" isn't a very catchy phrase. Can anyone coin a better one? (Or, is there already a better one that I don't know about?)
_vdpp 4y ago
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.
- AnimalMuppet 4y ago
  The first such successful lawsuit is going to change the landscape. Not just "somewhat" - it's going to be a massive change.
  - petergeoghegan 4y ago
    This sounds like motivated reasoning to me. Have you heard of Therac-25? You might be inclined to suggest that that could have been prevented if only they'd used formal methods. Perhaps that's true. It's something that could have been prevented in many different ways, though. Yet it still happened.
    - AnimalMuppet 4y ago
      Hmm. If I recall correctly, Therac-25 destroyed the company. It (and incidents like it) led the FDA to gradually be more stringent on scrutinizing software in medical devices. And yet, to the best of my knowledge, even the FDA has not mandated formal verification of the embedded software in medical devices. And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. It changed software, but only a little bit. Very little, given the magnitude of what happened.
      - petergeoghegan 4y ago
        > And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. It changed software, but only a little bit. There seems to have been something akin to an "accident chain", where a large number of things went wrong. Had any one of these things not happened, there might have been much less harm caused, or even no harm at all. I will admit to being peevish about stuff like this. Some of the failures with Therac-25 were systems failures that had nothing to do with software per se (I'm not counting "software hubris" as a software problem). They were failures of process, problems with hardware interlocks, and even UI bugs that made the software confusing to operators. I have nothing against formal methods, but they're no substitute for a deep and abiding paranoia.
yodsanklai 4y ago
Even regular static type-checking is seen as a burden by many programmers.

by daenz 4y ago

KSteffensen 4y ago

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 4y ago
"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 4y ago

> 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 4y ago
>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 4y ago
  > 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.
  - deleted 4y ago
    [deleted]
  - daenz 4y ago
    >Ever heard of this thing called ransomware, for example? Identity theft? Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. >Obviously the answer is that they could profit more and be happier. Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly?
    - guerrilla 4y ago
      > Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. > Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly? The revenue could come from savings on fixing bugs, paying for ransomed assets and all other costs that come from bugs. You're just assuming that doesn't add up and that there's no other reason that we don't do formal verification. That's just stupid. Show me the studies. Your claim is just as strong as the claim you think I'm making, but you missed my point entirely.

shoo 4y ago

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.

chmod600 4y ago
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".
- 4y ago

marcosdumay 4y ago

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?

AnimalMuppet 4y ago
This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Those provide formal verification of some aspects of the code. And that's great! It's progress! Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation that "it's amazing how many bugs there can be in a formally verified program" is no longer true.)
- marcosdumay 4y ago
  Well, the article has quite a list of "some aspects" of your code the author is working on. I have no reason why any of them could not be successful. I don't expect all of them to be, but anyone that gets there is already a huge advance.
- topspin 4y ago
  > This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Yes indeed. That is insightful. Is there a name for this process?
  - AnimalMuppet 4y ago
    Well, in AI, the process is called "AI can never succeed". So maybe the general thing is "X can never succeed", where X is some hugely ambitious (and ambiguous) thing, like "AI" or "formal software verification" or "curing cancer". We're probably never going to cure cancer - that is, have some treatment that conquers all cancers. Instead, we get "for this specific type of cancer, for these specific conditions, this treatment has a higher survival rate than the ones we had before". Over time, that adds up to a lot of people living out their days rather than dying early. And maybe software verification is the same. Enough ways of verifying specific aspects of software, and bugs have fewer places to hide. It won't find all bugs, but we'll still get better software. But "X can never succeed" isn't a very catchy phrase. Can anyone coin a better one? (Or, is there already a better one that I don't know about?)

_vdpp 4y ago

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.

AnimalMuppet 4y ago
The first such successful lawsuit is going to change the landscape. Not just "somewhat" - it's going to be a massive change.
- petergeoghegan 4y ago
  This sounds like motivated reasoning to me. Have you heard of Therac-25? You might be inclined to suggest that that could have been prevented if only they'd used formal methods. Perhaps that's true. It's something that could have been prevented in many different ways, though. Yet it still happened.
  - AnimalMuppet 4y ago
    Hmm. If I recall correctly, Therac-25 destroyed the company. It (and incidents like it) led the FDA to gradually be more stringent on scrutinizing software in medical devices. And yet, to the best of my knowledge, even the FDA has not mandated formal verification of the embedded software in medical devices. And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. It changed software, but only a little bit. Very little, given the magnitude of what happened.
    - petergeoghegan 4y ago
      > And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. It changed software, but only a little bit. There seems to have been something akin to an "accident chain", where a large number of things went wrong. Had any one of these things not happened, there might have been much less harm caused, or even no harm at all. I will admit to being peevish about stuff like this. Some of the failures with Therac-25 were systems failures that had nothing to do with software per se (I'm not counting "software hubris" as a software problem). They were failures of process, problems with hardware interlocks, and even UI bugs that made the software confusing to operators. I have nothing against formal methods, but they're no substitute for a deep and abiding paranoia.

yodsanklai 4y ago

Even regular static type-checking is seen as a burden by many programmers.