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.
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?
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...
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.
The places where you do see formal-methods would be in, for example, FADEC for aircraft engines, or an operating system process scheduler.
As it is, I don't know what part of the system is responsible for reporting money stolen by postmasters - the BBC News article is light on technical details. The Register has more details: https://www.theregister.com/2021/04/23/post_office_scandal_f... as does this website focused entirely on the trial: https://www.postofficetrial.com/2019_03_25_archive.html
The bugs are described as being part of the systems' payments processing system (as the Post Office does function as a financial institution, after-all) - but that at least some of the bugs were caused by ad-hoc work on the system (wot, no CI/CD to gatekeep releases?!) so I'm thinking this is just institutional incompetence - let alone a lack of software-engineering processes - so the idea of them implementing formal-methods for proving the system's correctness is laughable.
[1] https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-...
Imagine not doing inspections of new building construction because it would be costly.
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.
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.