[HN Gopher] A commemoration of Edsger Dijkstra [pdf]
___________________________________________________________________
A commemoration of Edsger Dijkstra [pdf]
Author : cion
Score : 121 points
Date : 2021-07-11 06:03 UTC (2 days ago)
(HTM) web link (www.cs.utexas.edu)
(TXT) w3m dump (www.cs.utexas.edu)
| tomcam wrote:
| Lovely. My favorite is by Klaus Wirth. One passage:
|
| > Occasionally he used a long "reading pipe", until once, deep in
| thought, he bumped it into a door and hurt himself in the throat.
| Then he switched to cigarettes.
| microtherion wrote:
| Wirth also did not shrink back from laying out some of his
| philosophical differences with Dijkstra:
|
| "One of Edsger's most peculiar idiosyncrasies (after 1970) was
| his vow never to use a computer."
|
| "Edsger had contributed significantly to a well-founded,
| rigorous approach to programming, in establishing it as an
| engineering science. I therefore awaited eagerly the appearance
| of a textbook, a fundamental guide to programming from his pen.
| But he had lost his interest in this endeavor, and instead
| concentrated exclusively on mathematical treatments and
| theories."
| romesmoke wrote:
| Who computer scientists of today could, in your opinion, be
| considered Dijkstra's spiritual successors?
| bordercases wrote:
| The key insight of Dijkstra is that we should use a kind of
| substitution calculus to derive programs from invariants.
|
| From Dijkstra's time we've seen partial adoptions and spinoffs
| from these insights. Using lambda calculus and static types
| gets you program behavior that looks a lot like refinement
| calculus and invariants (since types label domains that are
| equivalent to predicate sets, and lambda calculus computation
| _is_ the substitution model).
|
| For that reason I would say that the spiritual successor's to
| Dijsktra are in the functional programming community,
| particularly Haskell and Scala: Erik Meijer, Richard Bird,
| Martin Sapolsky, etc.
|
| Carnegie Mellon's Computer Science curriculum is also fairly
| integrated across the board to use this style of programming
| and mathematics.
| User23 wrote:
| > The key insight of Dijkstra is that we should use a kind of
| substitution calculus to derive programs from invariants.
|
| It baffles me that the "formal methods" (it really should be
| called automated methods) crowd not only ignores this lesson,
| but is completely blind to it. In my direct experience, the
| ones I've spoken to are so obsessed with verification that
| the idea of constructing a program that has specified
| properties apparently isn't even thinkable for them. Perhaps
| it's a defect in my ability to explain things, but I've never
| once managed to explain to one of them that construction is a
| significantly easier task than verification. It's a real
| shame because they're very intelligent people that I'm
| certain could contribute greatly to formal program
| derivation. I suppose it's one of those "professional
| deformations" Dijkstra occasionally mentions. One of the
| things I'd like to do when I have copious free time is build
| an Emacs mode that only allows edits that preserve the given
| invariants, perhaps using TLA+ or something similar.
|
| Anyone that wants to learn more on the subject of deriving
| programs should read one or both of A Discipline of
| Programming[1] or Predicate Calculus and Program
| Semantics[2]. The former is more approachable for the
| programmer who isn't as inclined toward formal mathematics.
| The latter basically takes the same concepts and treats them
| with much greater mathematical rigor.
|
| [1] https://www.goodreads.com/book/show/2276288.A_Discipline_
| of_...
|
| [2] https://www.goodreads.com/book/show/3144463-predicate-
| calcul...
| wooptoo wrote:
| D.J. Bernstein maybe?
| iamcurious wrote:
| There is mathmeth.com, also Ralph-Johan Back, also to some
| extent me (search for "foundations for mathematical
| methodology").
| User23 wrote:
| Leslie Lamport immediately comes to mind. His work extending
| predicate transformers for concurrency[1] is a good example.
|
| Edit: Tony Hoare isn't a successor, but he's a living genius
| who shares many of Dijkstra's inclinations.
|
| [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf
| enriquto wrote:
| Very interesting document, and many new photos! Love how Knuth
| explains how he had to be cautious around Dijkstra. He was truly
| the Chuck Norris of computing (badass, beard, and from Texas).
| berkes wrote:
| From Texas?
|
| He's from Rotterdam, The Netherlands. He worked and lived most
| of his life in The Netherlands and lived and worked about 15
| years in Texas, according to Wikipedia.
| munificent wrote:
| Not every Texan has the luxury of being born there.
| enriquto wrote:
| Sure! but if you read the texts you'll see that he sort of
| "adopted" a Texan persona when living there.
| iamcurious wrote:
| Haha, maybe a bit. But he was also very conscious of the
| different mindsets between Europe and America (and he
| firmly stood in the European mindset). Read "on the fact
| that the atlantic has two sides"
| rramadass wrote:
| Great article! I always have Edsger Dijkstra on a pedestal. The
| reason is his uncompromising attitude and biting wit in getting
| his beliefs across. I believe it is the only way to advance
| "Scientific Temperament".
|
| As Sherlock Holmes observes; _Pshaw, my dear fellow, what do the
| public, the great unobservant public, who could hardly tell a
| weaver by his tooth or a compositor by his left thumb, care about
| the finer shades of analysis and deduction!_ ; we the "great
| unobservant programming public" when it comes to mathematical
| underpinnings of Computer Programming need to be taught and
| frequently reminded of the importance of "logical analysis and
| proof deduction". :-)
| cafard wrote:
| I disagree about the reason. Dijkstra is too often remembered
| as an insult comic, in the same way that it is too easy to
| remember Schopenhauer as the guy who said snotty things about
| Hegel, Schelling, etc.
| User23 wrote:
| In my observation the people that remember him as an insult
| comic have only the most superficial acquaintance with the
| man and his work.
|
| That said, his non-technical EWDs can be pretty cutting. He
| didn't suffer those whom he saw as fools gladly. At least in
| his writings his humor is extremely dry.
| User23 wrote:
| Dijkstra has been an intellectual hero of mine as well. His
| book A Discipline of Programming pretty much completely altered
| my perspective of programming and reading through the majority
| of the English language EWDs was a very rewarding experience. I
| love his proof format. He was one of those rare geniuses who
| bothered to make his process public. His contempt for what he
| calls "rabbits"[1] is an expression of that devotion to
| intellectual honesty.
|
| [1] A rabbit in this context is a result that is a surprise, as
| if it had been pulled out of a hat.
| doesnotexist wrote:
| Dijkstra had a unique format for his undergraduate class where
| the entire grade basically came down to an interview at the end
| of the semester. During which he asked you to work out a solution
| to a problem in front of him one on one. A friend had the most
| memorable interaction with him during the interview/final exam.
| Dijkstra explained the problem and they began furiously writing
| out a solution in pencil getting a few lines into the proof
| before realizing they had made a mistake and began to erase what
| was written. Dijkstra responded "tsk tsk tsk, you are a rash
| mathematician" and advised the student to "Use a pen instead of
| pencil it will encourage you to spend more time with your
| thoughts before writing."
|
| A couple years later I saw a quote that reminded me of that
| interaction and it goes "I mean, if 10 years from now, when you
| are doing something quick and dirty, you suddenly visualize that
| I am looking over your shoulders and say to yourself "Dijkstra
| would not have liked this", well, that would be enough
| immortality for me."
|
| Dijkstra's ghost haunts us all.
| tda wrote:
| The exam in interview form is called an oral examination (vs
| written examination) and in my university in the Netherlands
| they were not that rare, especially for exams in the senior
| years where class sizes are smaller.
| xputer wrote:
| Interesting, thanks! Here is a link for mobile readers:
| https://outline.com/pcYcSh
___________________________________________________________________
(page generated 2021-07-13 23:02 UTC)