3 ms·

If so, this may be a good back-to-reality counter-example for all the over-zealous formal proof enthusiasts. There is an old paper from 70's by people who desig

If so, this may be a good back-to-reality counter-example for all the over-zealous formal proof enthusiasts. There is an old paper from 70's by people who designed complex systems where they stress the point that even if your system was designed and formally checked and if it obeys all the known rules and specifications, it will still fail in real world unless you test and iterate it a lot. Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. One has to experiment/iterate to find the very specifications that are then going to be designed against. Which in 737Max case was seemingly neglected.

hobofan 7y ago
> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. Is that so? Wouldn't it be in theory possible to verify it against our current understanding of all laws of physics and the corresponding equations?
- nutjob2 7y ago
  It also has a user interface. Are you saying it's possible to formally quantify human behaviour as well?
  - hobofan 7y ago
    Every program has a inputs, and with that some more ore less direct version of a user interface. You define the acceptable input values and then define what happens with unacceptable ones (and same for combinations). If that were not verifiable, then no program would be.
- posix_me_less 7y ago
  You are forgetting nondeterministic aspects. Only in theory, aircraft and atmosphere is a deterministic Newtonian machine, in practice, less so. But even if so, physics simulations can't be done and evaluated for all possible initial conditions for even the simplest model. One can imagine a mental model of airplane and make a formal design for it. Then do a formal check in the most important scenarios that introduce weather, human action, system failures. The design will always fail for some scenarios. Not a problem if those are not important (in terms of risk). But which scenarios are the important ones? Probability and severity of consequences of those scenarios are much needed knowledge, and one can find those only via the good old method of iterative testing in wild.
- ori_b 7y ago
  But it obeys the laws of physics perfectly as it nosedives into the ground.
mannykannot 7y ago
> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. You cannot exhaustively test software either - the number of cases to cover are beyond astronomical. The effectiveness of both specification and testing ultimately depend on the same thing: thinking of all the relevant possibilities. If you overlook a possible failure mode, there's no guarantee it will be caught at any phase. The main benefit of formal methods, I think, is that the rigor tends to make such oversights visible. the only people who think formal methods are a magic bullet are those who have not tried them. Likewise, the only people who think more testing (and especially unit testing) is a magic bullet are those who don't understand combinatorial complexity.

hobofan 7y ago

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. Is that so? Wouldn't it be in theory possible to verify it against our current understanding of all laws of physics and the corresponding equations?

nutjob2 7y ago
It also has a user interface. Are you saying it's possible to formally quantify human behaviour as well?
- hobofan 7y ago
  Every program has a inputs, and with that some more ore less direct version of a user interface. You define the acceptable input values and then define what happens with unacceptable ones (and same for combinations). If that were not verifiable, then no program would be.
posix_me_less 7y ago
You are forgetting nondeterministic aspects. Only in theory, aircraft and atmosphere is a deterministic Newtonian machine, in practice, less so. But even if so, physics simulations can't be done and evaluated for all possible initial conditions for even the simplest model. One can imagine a mental model of airplane and make a formal design for it. Then do a formal check in the most important scenarios that introduce weather, human action, system failures. The design will always fail for some scenarios. Not a problem if those are not important (in terms of risk). But which scenarios are the important ones? Probability and severity of consequences of those scenarios are much needed knowledge, and one can find those only via the good old method of iterative testing in wild.
ori_b 7y ago
But it obeys the laws of physics perfectly as it nosedives into the ground.

mannykannot 7y ago

> Because it is impossible to formally specify all possibilities that can happen, and noone can forecast all the desired specs before the thing is built and tested in real. You cannot exhaustively test software either - the number of cases to cover are beyond astronomical. The effectiveness of both specification and testing ultimately depend on the same thing: thinking of all the relevant possibilities. If you overlook a possible failure mode, there's no guarantee it will be caught at any phase. The main benefit of formal methods, I think, is that the rigor tends to make such oversights visible. the only people who think formal methods are a magic bullet are those who have not tried them. Likewise, the only people who think more testing (and especially unit testing) is a magic bullet are those who don't understand combinatorial complexity.