4 ms·
> if you believe that computing cannot scale without correctness. He was wrong about that one thing, and to be fair to him, it's still a little amazing in retro
by munificent 6y ago
> if you believe that computing cannot scale without correctness. He was wrong about that one thing, and to be fair to him, it's still a little amazing in retrospect,
That is clearly wrong if one is willing to take a moment to stop gazing at the wonder of pure mathematics and look at the outside world. There is no notion of "correctness" for the pyramids of Egypt, the dykes of the Netherlands, Milan Cathedral, or the world economy and yet those huge-scale systems all function.
> Dijkstra's pessimism and his use of harsh, attention-getting language makes a lot of sense.
It makes sense in terms of Dijkstra's personality, but it makes no logical sense. If you believe mathematical correctness is such a valuable principle, then you should be able to leverage that same principle in one's own arguments. The fact that Dijkstra couldn't dispassionately prove that correctness was vital and had to resort to emotionally-loaded weasel words undermines his own claim.
- watwut 6y agoImo, the real issue is that people seem to think that smart mathematicians or scientists don't argue like normal people, don't get emotional when arguing and always talk from divine truth. The issue have nothing to do with mathematical correctness, so you can't apply the same principles. This is not math. But, Dijkstra's it's not being logical in arguments, because he is not of dick and likely this style of arguing was working for him in his life.
- dkarl 6y ago> There is no notion of "correctness" for the pyramids of Egypt, the dykes of the Netherlands, Milan Cathedral, or the world economy and yet those huge-scale systems all function. I think it's impossible to come up with a rational judgment of whether the world economy "functions." I mean, those of us who are alive are alive, but there are a lot of things that have happened that haven't been ideal. Besides the world economy, nothing you mention has the functional complexity of a large piece of software, and none of it was designed and built with much confidence, other than confidence that came from similarity to previous designs, and from an optimistic outlook that issues encountered during construction could be coped with. This wall is cracking, so we tear it down and rebuild it a little thicker. We have a few centuries, after all. I think you're right that modern software projects are analogous to ancient pyramids and medieval cathedrals. That's pretty much where we are. Yet somehow, working at that low level of sophistication, we've built working software that is orders of magnitude more complex than cathedrals. I'm not saying I know how to improve on the situation, or even that we can; I'm just pointing out how different it is from, say, contemporary structural engineering where we can analyze the design of a novel structure and have a pretty good idea of whether it will be safe based on its geometry and known characteristics of materials and how they're joined. It's amazing that we've reached the scale we have with nothing comparable. > If you believe mathematical correctness is such a valuable principle, then you should be able to leverage that same principle in one's own arguments. The idea that mathematical reasoning is on some spectrum with dispassionate discourse has motivated hundreds of years of attempts to improve natural language by making it more mathematical. Result: some interesting contributions to philosophy but very little change in how people communicate. People are still people.
- ThenAsNow 6y ago> That is clearly wrong if one is willing to take a moment to stop gazing at the wonder of pure mathematics and look at the outside world. There is no notion of "correctness" for the pyramids of Egypt, the dykes of the Netherlands, Milan Cathedral, or the world economy and yet those huge-scale systems all function. Wow, couldn't disagree with this more, at least on your examples of civil engineering (buildings, dikes). There are testable, comprehensive physical principles that govern whether any of these engineered products function in their most fundamentally-intended ways. This is the reason most buildings are resilient and don't collapse under load, or that dams keep water from flowing uncontrolled. You can debate "correctness" in the sense of the purpose the product serves, but there is the principle of correctness of construction which your civil engineering examples (and anything truly engineered) satisfy. Correctness in construction is not subjective.
- munificent 6y ago> There are testable, comprehensive physical principles that govern whether any of these engineered products function in their most fundamentally-intended ways. 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".
- ThenAsNow 6y agoWhen 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.