4 ms·

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 funct

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 5y 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 5y ago
  Thats fine, but if they choose to handle money with a joke app, they should eat the losses
Mauricebranagh 5y ago
More than that there was at least one Suicide
DaiPlusPlus 5y 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.
- da_chicken 5y ago
  You don't need a formal proof for the entire system as a whole. You could simply have a formal proof of specific functions of the software. Those functions which will have their data audited, for example.
  - DaiPlusPlus 5y ago
    Correct - but this is a line-of-business application software: so I'm assuming that everything about it is subject to changes. The parts of the system that would be thoroughly spec'd out, QA'd (and maybe do have formal proofs) would be the underlying database system they're using which would be a third-party system like Oracle or Sybase or MS SQL (I just hope they're not using Progress/OpenEdge...). 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_fujitsu_convictions_quashed/ 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 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.
justincormack 5y ago
That wasn't the issue. Fujitsu, who operated the system, had access to post office branch systems with full access, but this was denied. The postmasters were prosecuted individually without good enough representation. The 2019 judgement is a good read about how the prosecutions happened and how the evidence was presented [1]. Really, formal methods and bugs were not issues, this was a system with humans in and someone decided that some of the humans should be blamed for issues, because the balance of power let them. [1] https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-post-office-judgment.pdf https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-...

himinlomax 5y 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 5y ago
Thats fine, but if they choose to handle money with a joke app, they should eat the losses

Mauricebranagh 5y ago

More than that there was at least one Suicide

DaiPlusPlus 5y 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.

da_chicken 5y ago
You don't need a formal proof for the entire system as a whole. You could simply have a formal proof of specific functions of the software. Those functions which will have their data audited, for example.
- DaiPlusPlus 5y ago
  Correct - but this is a line-of-business application software: so I'm assuming that everything about it is subject to changes. The parts of the system that would be thoroughly spec'd out, QA'd (and maybe do have formal proofs) would be the underlying database system they're using which would be a third-party system like Oracle or Sybase or MS SQL (I just hope they're not using Progress/OpenEdge...). 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_fujitsu_convictions_quashed/ 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 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.

justincormack 5y ago

That wasn't the issue. Fujitsu, who operated the system, had access to post office branch systems with full access, but this was denied. The postmasters were prosecuted individually without good enough representation. The 2019 judgement is a good read about how the prosecutions happened and how the evidence was presented [1]. Really, formal methods and bugs were not issues, this was a system with humans in and someone decided that some of the humans should be blamed for issues, because the balance of power let them. [1] https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-post-office-judgment.pdf https://www.judiciary.uk/wp-content/uploads/2019/12/bates-v-...