3 ms·

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 hig

by _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.
    - _vdpp 4y ago
      Granted it was 1982, before software played such a big role in everyone’s life. Maybe it would be a bigger deal now.
    - hwayne 4y ago
      The company is still around and still makes hundreds of millions in revenue. https://en.wikipedia.org/wiki/Atomic_Energy_of_Canada_Limited https://en.wikipedia.org/wiki/Atomic_Energy_of_Canada_Limite...
- lelanthran 4y ago
  > 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.
lelanthran 4y ago
> 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.

by _vdpp 4y ago

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.
  - _vdpp 4y ago
    Granted it was 1982, before software played such a big role in everyone’s life. Maybe it would be a bigger deal now.
  - hwayne 4y ago
    The company is still around and still makes hundreds of millions in revenue. https://en.wikipedia.org/wiki/Atomic_Energy_of_Canada_Limited https://en.wikipedia.org/wiki/Atomic_Energy_of_Canada_Limite...
lelanthran 4y ago
> 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.

lelanthran 4y ago

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