Re:How do we tell truths that might hurt? (1975)
by ThenAsNow on Thursday October 15, 2020 @06:46PM
(#24795181)
When we determine if an aircraft trims, or a boat floats, it is not correct to say it is statistical engineering test of the probability of failure. You formalize the properties the system must have in order to not fail, and you use conservation equations to ultimately compute whether or not the system satisfies those properties. Margins are used to account for parameters that have uncertainty attached. All of these elements are subject to symbolic mathematical formalism. One can quite clearly state the inequalities that must be satisfied to be, e.g., controllable.
It's unclear how this would be any different than mathematically formalizing a distributed system, identifying the properties that constitute correctness of operation of that distributed system, and symbolically proving that subject to certain assumptions, the distributed system model does or does not satisfy those properties. This would presumably be consistent with the Dijkstra view of mathematical correctness.
These are statistical engineering tests of the probability of failure under certain conditions. That is not at all what Dijkstra would consider to be "correctness". Dijkstra is talking about mathematical proof. In mathematics, one does not say "1 + 2 = 3 plus or minus 0.1 with a safety factor of 2".