4 ms·

I agree. Reasoning about correctness can be a very powerful tool for some of the algorithmic parts of a system. But large parts of a system are not really amena

I agree. Reasoning about correctness can be a very powerful tool for some of the algorithmic parts of a system. But large parts of a system are not really amenable to formal reasoning about correctness. As an example, if you try to write our own web search engine, the linear algebra or neural network operations you may be using are certainly amenable to mathematical reasoning, but the relevancy of the returned results is not something you can prove mathematically. And in my opinion, this fact often leads "correctness" fanatics to retreat to safe areas where their methods work, and snipe at all the rest of the world. Characteristically, the article quotes E.W.Dijkstra, whose much beloved notes are full of explorations of mathematical toy problems, and catty dismissals of anybody trying to make real world use of computers. When Knuth was dissatisfied with the results of early computer typesetting, he spent years of his life developing TeX. Meanwhile, Dijkstra kept hand writing his papers and having staff turn them into printed form. That, to me, is the epitome of the "correctness über alles" mindset.

Jtsummers 8y ago
That seems to be an unfair assessment of Dijkstra's interests and activities. He made major contributions in algorithms, language design, concurrent computing, and distributed contributing, among other fields. He is basically the face of the Structured Programming movement (and coined the term) which led to the common design elements of many languages used today (both the presence of certain elements, and the absence of others). I think it'd do you some good to read a bit more of his work and the history of computing.
- microtherion 8y ago
  There's a good chance I have read more of his work than you have. Yes, Dijkstra made major contributions to algorithms—exactly the "safe corner" where correctness thinking applies. Ironically, one of his contributions was to the concept of semaphores. I sure don't hear any of Dijkstra's fans claim today that if distributed programs just used semaphores, all our concurrency problems would be solved. Another important contribution: The Banker's algorithm, of which Andrew Tanenbaum observed (Modern Operating Systems, 2nd ed): > The banker’s algorithm was first published by Dijkstra in 1965. Since that time, nearly every book on operating systems has described it in detail. Innumerable papers have been written about various aspects of it. Unfortunately, few authors have had the audacity to point out that although in theory the algorithm is wonderful, in practice it is essentially useless because processes rarely know in advance what their maximum resource needs will be. In addition, the number of processes is not fixed, but dynamically varying as new users log in and out. Furthermore, resources that were thought to be available can suddenly vanish (tape drives can break). Thus in practice, few, if any, existing systems use the banker’s algorithm for avoiding deadlocks. ... which is pretty much my argument: Dijkstra picked himself the neat little corner that WAS amenable to mathematical reasoning, at the expense of real world applicability. One of Dijkstra's contributions to language design was resigning from the Algol 68 committee. It might do proponents of formal methods good to reflect on why that language was less than a stellar success, given how strongly it relied on advanced formal descriptions. But the question is not whether Dijkstra contributed to algorithms, language design, or concurrent+distributed computing (he certainly did). The thesis that the Article presents (and supports by quoting Dijkstra, who did agree with that thesis) is that formal methods apply universally in system design, and that today's software woes are largely the result of insufficient application of formal methods. It is there that I disagree, and that Dijkstra kept pontificating about despite having abolished programming and using computers around the time he started focusing on formal methods. And that detachment from and disdain of the actual practice of computer use is what renders his later opinions suspect to me.

Jtsummers 8y ago

That seems to be an unfair assessment of Dijkstra's interests and activities. He made major contributions in algorithms, language design, concurrent computing, and distributed contributing, among other fields. He is basically the face of the Structured Programming movement (and coined the term) which led to the common design elements of many languages used today (both the presence of certain elements, and the absence of others). I think it'd do you some good to read a bit more of his work and the history of computing.

microtherion 8y ago
There's a good chance I have read more of his work than you have. Yes, Dijkstra made major contributions to algorithms—exactly the "safe corner" where correctness thinking applies. Ironically, one of his contributions was to the concept of semaphores. I sure don't hear any of Dijkstra's fans claim today that if distributed programs just used semaphores, all our concurrency problems would be solved. Another important contribution: The Banker's algorithm, of which Andrew Tanenbaum observed (Modern Operating Systems, 2nd ed): > The banker’s algorithm was first published by Dijkstra in 1965. Since that time, nearly every book on operating systems has described it in detail. Innumerable papers have been written about various aspects of it. Unfortunately, few authors have had the audacity to point out that although in theory the algorithm is wonderful, in practice it is essentially useless because processes rarely know in advance what their maximum resource needs will be. In addition, the number of processes is not fixed, but dynamically varying as new users log in and out. Furthermore, resources that were thought to be available can suddenly vanish (tape drives can break). Thus in practice, few, if any, existing systems use the banker’s algorithm for avoiding deadlocks. ... which is pretty much my argument: Dijkstra picked himself the neat little corner that WAS amenable to mathematical reasoning, at the expense of real world applicability. One of Dijkstra's contributions to language design was resigning from the Algol 68 committee. It might do proponents of formal methods good to reflect on why that language was less than a stellar success, given how strongly it relied on advanced formal descriptions. But the question is not whether Dijkstra contributed to algorithms, language design, or concurrent+distributed computing (he certainly did). The thesis that the Article presents (and supports by quoting Dijkstra, who did agree with that thesis) is that formal methods apply universally in system design, and that today's software woes are largely the result of insufficient application of formal methods. It is there that I disagree, and that Dijkstra kept pontificating about despite having abolished programming and using computers around the time he started focusing on formal methods. And that detachment from and disdain of the actual practice of computer use is what renders his later opinions suspect to me.