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.