3 ms·
>critical software goes under a much more rigorous testing regime Testing is not only not enough, it's also not required :) (as Dijkstra said, it can only show
by jffhn 7y ago
>critical software goes under a much more rigorous testing regime
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 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).
- jammygit 7y agoWhen 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?
- jffhn 7y agoYes, 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).