4 ms·

was this something to do with Djykstra's work?

by caycep 3y ago

maleldil 3y ago
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.
- Scarblac 3y ago
  Also, think of ij as a single letter, quite like a y but with dots.
  - mettamage 3y ago
    That's what they taught me in elementary school! :D
  - dekhn 3y ago
    https://en.wikipedia.org/wiki/IJ_(digraph) https://en.wikipedia.org/wiki/IJ_(digraph)
- smokel 3y ago
  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.
- klyrs 3y ago
  I've always thought the ijk were quaternions and the alternative spelling would be D-1stra.
wisnesky 3y ago
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).
throwaway17_17 3y ago
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.
User23 3y ago
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/EWD288.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD375.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E... [3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD803/EWD803.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E... [4] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/EWD1157.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/E... [5] https://en.wikipedia.org/wiki/Abstract_nonsense https://en.wikipedia.org/wiki/Abstract_nonsense
marcosdumay 3y ago
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.

was this something to do with Djykstra's work?

by caycep 3y ago

was this something to do with Djykstra's work?

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.

Scarblac 3y ago
Also, think of ij as a single letter, quite like a y but with dots.
- mettamage 3y ago
  That's what they taught me in elementary school! :D
- dekhn 3y ago
  https://en.wikipedia.org/wiki/IJ_(digraph) https://en.wikipedia.org/wiki/IJ_(digraph)
smokel 3y ago
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.
klyrs 3y ago
I've always thought the ijk were quaternions and the alternative spelling would be D-1stra.

wisnesky 3y ago

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).

throwaway17_17 3y ago

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.

User23 3y ago

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/EWD288.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E... [2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD375.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E... [3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD803/EWD803.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/E... [4] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/EWD1157.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/E... [5] https://en.wikipedia.org/wiki/Abstract_nonsense https://en.wikipedia.org/wiki/Abstract_nonsense

marcosdumay 3y ago

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.