6 ms·

While I agree more broadly, you cannot expect the Post Office to prove a negative. How would they prove conclusively that the software had no bugs at all under

While I agree more broadly, you cannot expect the Post Office to prove a negative. How would they prove conclusively that the software had no bugs at all under any circumstances? That's a pretty steep QA bill imho.

jjk166 6y ago
They don't need to prove that their software has no bugs, but they do need to prove that what their software claims is true.
throwaway823882 6y ago
This is the proof that how we write software is inherently wrong, if we allow innocent lives to be destroyed because we don't want to write it differently. Imagine not doing inspections of new building construction because it would be costly.
- etothepii 6y ago
  The Grenfell inquiry would like to talk to you ...
- wutbrodo 6y ago
  > This is the proof that how we write software is inherently wrong, if we allow innocent lives to be destroyed because we don't want to write it differently. I think there's a lot of room for writing software better, including expanded source access for public systems and formal verification when critical. But the failure in this case isn't technical, it's legal. It's rational to decide that occasional bugs in a mail software system are acceptable, and not worth the cost of designing a system's development around formal-verification. What's obviously insane is treating such a system as if it's bug-free beyond a reasonable doubt, and ruining innocent people's lives over it. There are a lot of forms of gross incompetence and negligence that we're all fine with because they're so common. Failing to reason about software systems and their pitfalls, or consult with those who are capable of doing so, is an extremely-common and often-dangerous example (cf dumbass Senators grilling Zuckerberg with their 1970s understanding of how technology functions). The blame here lies squarely on the prosecutors, judges, etc who are responsible for these verdicts. They should be ashamed of themselves.
  - mcguire 6y ago
    As long as none of the blame goes to the programmers, we're all good.
    - wutbrodo 6y ago
      Sure, or some of us aren't so simple-minded that we only see things through the lens of the identity groups we belong to.
- guitarbill 6y ago
  That is a tempting conclusion, but consider if the software was 100% correct per some specification, and the spec was wrong? No, the problem is greater than that. Decisions that affect people should not be made solely by computers or algorithms, and those decisions should be made transparent and auditable. If that leads to different/better ways of writing software, good. It's a larger societal issue though.
jschwartzi 6y ago
They can actually use formal methods to prove that their software is bug free. This technique is often used in safety-critical systems to ensure that they function as-specified. As long as the specification is correct, the software system should perform to specification under all input conditions. https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods We should consider the cost of QA and of engineering process against the cost to these 39 people of their freedom and a large part of their lives due to an accounting error in the software.
- himinlomax 6y ago
  Formal methods require a comprehensive specification. Usually, if you have a specification comprehensive enough for formal verification, you already have 90% of the benefits, which is why it's (so far) only really useful in safety critical applications with a very small scope. I'm not going to take a huge risk in betting that the postal service didn't have anything resembling a serious spec in this case.
  - ClumsyPilot 6y ago
    Thats fine, but if they choose to handle money with a joke app, they should eat the losses
- Mauricebranagh 6y ago
  More than that there was at least one Suicide
- DaiPlusPlus 6y ago
  Formal proof of program correctness tends to require that the software's purpose lies in a very narrow, and extremely well-defined problem space. The _Horizon_ software in-question is a general-purpose line-of-business system, which presumably has to react to ever-changing business requirements - that's probably the hardest space to implement formal-methods in - with little benefit for doing-so precisely because requirements change so often. The places where you do see formal-methods would be in, for example, FADEC for aircraft engines, or an operating system process scheduler.
pmichaud 6y ago
Sure, I can agree with that — it’s way too hard to prove a big system isn’t buggy. So then you also can’t use its output as evidence in court, right? You have to have other evidence that you can prove isn’t faulty. Can’t have it both ways.
davidhyde 6y ago
Agreed that you cannot expect the Post Office to prove a negative but, if they cannot prove a negative, they should not be able to use their computer system as evidence of theft and fraud. Especially if this is the only evidence they have.
- ganzuul 6y ago
  So government software, technically cybernetic software, should be proven to be correct. Will automatic theorem proovers be able to accommodate this?
  - _vertigo 6y ago
    Not necessarily proven to be correct, proven to be correct _beyond a reasonable doubt_. That's the standard.
bennysomething 6y ago
If you are taking someone to court, maybe be cautious, could it be a bug, are there similarities across the all cases here? Etc.
ClumsyPilot 6y ago
If their code is a mess and has errors, and there are people at post office that know this, they should be fined on the spot for false representation of contemp of the court. If their system were up to date, written in a safe language, has unit tests and an independant review said it was solid, then it is just one acceptable piece of evidence. What i dont get is - where was the money? Supposedly hundreds of people stoke huge amount of money, and none of them had it in a bank, bought a new car, or showed any signs of suddenly becoming wealthier. Where did the judge think the money go to, they ate it? How was this not suspicious?
- LatteLazy 6y ago
  The amazing thing about these cases are exactly how many shitty things had to happen (and did) for this to occur. Like you say, where is the money? And why didn't anyone spot that more sub-post-masters were getting charged than almost all other employee types? Why didn't anyone manage to reproduce the error? Why did managers hide the reports (who does that?)? I personally think this is partly down to the fact people don't get state defence lawyers anymore in the uk. You could accuse me of fraud with zero evidence and I likely would have to plead guilty as I don't have 20k for the down payment for a lawyer... What a shit storm. Now watch as nothing changes...

jjk166 6y ago

They don't need to prove that their software has no bugs, but they do need to prove that what their software claims is true.

throwaway823882 6y ago

This is the proof that how we write software is inherently wrong, if we allow innocent lives to be destroyed because we don't want to write it differently. Imagine not doing inspections of new building construction because it would be costly.

etothepii 6y ago
The Grenfell inquiry would like to talk to you ...
wutbrodo 6y ago
> This is the proof that how we write software is inherently wrong, if we allow innocent lives to be destroyed because we don't want to write it differently. I think there's a lot of room for writing software better, including expanded source access for public systems and formal verification when critical. But the failure in this case isn't technical, it's legal. It's rational to decide that occasional bugs in a mail software system are acceptable, and not worth the cost of designing a system's development around formal-verification. What's obviously insane is treating such a system as if it's bug-free beyond a reasonable doubt, and ruining innocent people's lives over it. There are a lot of forms of gross incompetence and negligence that we're all fine with because they're so common. Failing to reason about software systems and their pitfalls, or consult with those who are capable of doing so, is an extremely-common and often-dangerous example (cf dumbass Senators grilling Zuckerberg with their 1970s understanding of how technology functions). The blame here lies squarely on the prosecutors, judges, etc who are responsible for these verdicts. They should be ashamed of themselves.
- mcguire 6y ago
  As long as none of the blame goes to the programmers, we're all good.
  - wutbrodo 6y ago
    Sure, or some of us aren't so simple-minded that we only see things through the lens of the identity groups we belong to.
guitarbill 6y ago
That is a tempting conclusion, but consider if the software was 100% correct per some specification, and the spec was wrong? No, the problem is greater than that. Decisions that affect people should not be made solely by computers or algorithms, and those decisions should be made transparent and auditable. If that leads to different/better ways of writing software, good. It's a larger societal issue though.

jschwartzi 6y ago

They can actually use formal methods to prove that their software is bug free. This technique is often used in safety-critical systems to ensure that they function as-specified. As long as the specification is correct, the software system should perform to specification under all input conditions. https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods We should consider the cost of QA and of engineering process against the cost to these 39 people of their freedom and a large part of their lives due to an accounting error in the software.

himinlomax 6y ago
Formal methods require a comprehensive specification. Usually, if you have a specification comprehensive enough for formal verification, you already have 90% of the benefits, which is why it's (so far) only really useful in safety critical applications with a very small scope. I'm not going to take a huge risk in betting that the postal service didn't have anything resembling a serious spec in this case.
- ClumsyPilot 6y ago
  Thats fine, but if they choose to handle money with a joke app, they should eat the losses
Mauricebranagh 6y ago
More than that there was at least one Suicide
DaiPlusPlus 6y ago
Formal proof of program correctness tends to require that the software's purpose lies in a very narrow, and extremely well-defined problem space. The _Horizon_ software in-question is a general-purpose line-of-business system, which presumably has to react to ever-changing business requirements - that's probably the hardest space to implement formal-methods in - with little benefit for doing-so precisely because requirements change so often. The places where you do see formal-methods would be in, for example, FADEC for aircraft engines, or an operating system process scheduler.

pmichaud 6y ago

Sure, I can agree with that — it’s way too hard to prove a big system isn’t buggy. So then you also can’t use its output as evidence in court, right? You have to have other evidence that you can prove isn’t faulty. Can’t have it both ways.

davidhyde 6y ago

Agreed that you cannot expect the Post Office to prove a negative but, if they cannot prove a negative, they should not be able to use their computer system as evidence of theft and fraud. Especially if this is the only evidence they have.

ganzuul 6y ago
So government software, technically cybernetic software, should be proven to be correct. Will automatic theorem proovers be able to accommodate this?
- _vertigo 6y ago
  Not necessarily proven to be correct, proven to be correct _beyond a reasonable doubt_. That's the standard.

bennysomething 6y ago

If you are taking someone to court, maybe be cautious, could it be a bug, are there similarities across the all cases here? Etc.

ClumsyPilot 6y ago

If their code is a mess and has errors, and there are people at post office that know this, they should be fined on the spot for false representation of contemp of the court. If their system were up to date, written in a safe language, has unit tests and an independant review said it was solid, then it is just one acceptable piece of evidence. What i dont get is - where was the money? Supposedly hundreds of people stoke huge amount of money, and none of them had it in a bank, bought a new car, or showed any signs of suddenly becoming wealthier. Where did the judge think the money go to, they ate it? How was this not suspicious?

LatteLazy 6y ago
The amazing thing about these cases are exactly how many shitty things had to happen (and did) for this to occur. Like you say, where is the money? And why didn't anyone spot that more sub-post-masters were getting charged than almost all other employee types? Why didn't anyone manage to reproduce the error? Why did managers hide the reports (who does that?)? I personally think this is partly down to the fact people don't get state defence lawyers anymore in the uk. You could accuse me of fraud with zero evidence and I likely would have to plead guilty as I don't have 20k for the down payment for a lawyer... What a shit storm. Now watch as nothing changes...