Re:Boeing identifies new software problem on grounded 737 Max
by jammygit on Thursday February 06, 2020 @06:24PM
(#22261544)
When proving its correct, isn’t there always the possibility that the proof abstracted away some real world nuance into an assumption, and that assumption could be wrong?
Re:Boeing identifies new software problem on grounded 737 Max
by jffhn on Thursday February 06, 2020 @07:15PM
(#22261889)
Yes, I guess the proof is only relative to the formal spec, if the spec (formal or not) is nonsense it's another problem (so you might not have to test the program, but still have to test the complete system).
But I guess (again) that having formal specs getting proven helps to avoid inconsistent specs. I recall a talk by Martyn Thomas where he said that with these methods it was harder to get programs to compile (for example, the compiler could complain if it detected an inconsistency, either between the spec and the program or within the spec itself).
Testing is not only not enough, it's also not required :) (as Dijkstra said, it can only show the presence of bugs, not their absence)
For example, the software for some automated subways in France has never been tested, only proven correct (source: https://www.youtube.com/watch?v=jc9QmqKIUj4&t=54m50s).
Similar formal methods are used for critical software pieces in Airbus aircrafts (source: the same speaker as for the linked video, but I don't remember which talk that was in).