Just a head's up, there's an easy way to remember Dijkstra's spelling: D ijk stra. You know, ijk as the common loop indices.

Also, think of ij as a single letter, quite like a y but with dots.

That's what they taught me in elementary school! :D

Also, Dijkstra was from The Netherlands, and the word "dijk" is Dutch for dike, i.e. the water barrier.

"Dikestra" has a shorter path to the Dutch pronunciation than Djikstra.

I've always thought the ijk were quaternions and the alternative spelling would be D-1stra.

Yes, although Dijkstra was interested in proving programs correct in general, not just in how lambda calculi correspond to logics correspond to categories (a proof technique for program correctness, among other things).

As far as I am aware this doesn’t relate to much work done by Dijkstra. This is really the Type Theoretic computer science program. It starts at Church and progresses through Curry (inspired by Schoenfinkel), then hits the ‘modern’ academic lineage splitting in many directions. On the computer science side in America Constable and his doctoral students (Robert Harper included), Dana Scott, Strachey, Reynolds, the current CMU proof theory/type theory professors, and in Europe you have the French school with Coquand, Huet, etc from INRIA and the English lineage from Milner.

Obviously the above is a very truncated list and misses out on a huge chunk of formative thinkers, and doesn’t get to the cutting edge modern developments. Additionally, I’m leaving out the Math centric developments and people, like Mike Shulman, Dan Licata, etc.

I'm not sure. Dijkstra, despite his somewhat incorrect reputation as a curmudgeonly theorist who preferred pencils to computers, had a notable pragmatic streak. And, as a matter of pragmatism, he identified the close relationship between programs and proofs. There are many such examples in his writings, but here are a few[1][2][3][4]. It's particularly interesting to see how his thinking evolves. EWD288 in particular includes what I view as both good advice and a powerful refutation of a fallacy that is stubbornly popular even today:

  Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels.

I have myself applied this in "real" (aka, I got paid for it by a FAANG) programming by proving the correctness of the overall structure of a service (and verifying it with tests) while leaving implementation details for which requirements were nonexistent or unclear unspecified or underspecified. Since I'm neither as creative nor as clever as Dijkstra was I still like to write tests, but I've found that I can do TDD in a way that meshes cleanly with his program and proof construction style. The end result is I have code that I have both proved correct and that has solid test coverage. The tests are particularly useful for collaboration, because it's just not realistic to expect every team member who touches a piece of code to understand and rederive the appropriate parts of said proof. And as an added bonus, it escapes the common complaint for TDD that the tests get in the way of development. They don't when you only test what needs to be proved!

Edit: I find it amusing how much closer Dijkstra's approach is to what might be called "normal" (Algol-ish) programming compared to the Abstract Nonsense[5] favored by the category theorists. I wouldn't call it any less mathematical though. Dijkstra was very much a mathematical formalist as is clear to anyone who has made a study of his work or life.

[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...

[2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E...

[3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E...

[4] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/E...

[5] https://en.wikipedia.org/wiki/Abstract_nonsense

> I find it amusing how much closer Dijkstra's approach is to what might be called "normal" (Algol-ish) programming compared to the Abstract Nonsense[5] favored by the category theorists. I wouldn't call it any less mathematical though.

It's true that he mainly used a sequential, imperative notation for describing things, but it seems like later in his life, he preferred functional programming for teaching computer science to students. He petitioned the University of Texas to not switch from teaching it in Haskell to teaching it in Java for this reason.

https://www.cs.utexas.edu/users/EWD/OtherDocs/To%20the%20Bud...

A fundamental reason for the preference is that functional programs are much more readily appreciated as mathematical objects than imperative ones, so that you can teach what rigorous reasoning about programs amounts to. The additional advantage of functional programming with “lazy evaluation” is that it provides an environment that discourages operational reasoning.

This is all from research way older than Dijkstra.

It does have something to do with his work because his work extended it. But by that metric, it also has something to do with all of computer science, and a lot of mathematics.