3 ms·

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_

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

da_chicken 6y 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 6y 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.