4 ms·

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 whic

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.