Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A commemoration of Edsger Dijkstra [pdf]

cs.utexas.edu

Post reply on HN
Print view View original

21–27 of 27 posts

Re: A commemoration of Edsger Dijkstra [pdf]

#21

Post by User23 »

bordercases wrote: post #13
romesmoke wrote: post #5

Who computer scientists of today could, in your opinion, be considered Dijkstra's spiritual successors?

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 computatio…

> 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] and 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...

Re: A commemoration of Edsger Dijkstra [pdf]

#22

Post by rramadass »

User23 wrote: post #21
bordercases wrote: post #13

Earlier quoted context omitted.

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 computatio…

> 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 prop…

>Anyone that wants to learn more on the subject of deriving programs should read

Two more;

* EWD316 - A Short Introduction to the Art of Programming.

* A Method of Programming - Book co-authored with W.H.J.Feijen. For some reason, this is not well known though it was written as a course textbook. Draft version here: https://www.softwareresearch.net/fileadmin/src/docs/teaching...

Re: A commemoration of Edsger Dijkstra [pdf]

#23

Post by rramadass »

bordercases wrote: post #13
romesmoke wrote: post #5

Who computer scientists of today could, in your opinion, be considered Dijkstra's spiritual successors?

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 computatio…

Great insight! His idea of the "Weakest Precondition Calculus" is Functional in contrast to "Hoare Triples" which are Relational.

Re: A commemoration of Edsger Dijkstra [pdf]

#24

Post by rramadass »

microtherion wrote: post #17
tomcam wrote: post #3

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.

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 progr…

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

So Wirth himself decided to write it viz. Systematic Programming: An Introduction.

Re: A commemoration of Edsger Dijkstra [pdf]

#26

Post by e1e24b76 »

Will programming ever be free from the opinions of elitist hacks like Edsger Dijkstra ?

People with obsessive compulsive disorder, asperger and autism are unhirable in every profession on the planet. Every single profession - without exception. They are worthless as friends, worthless as parents, worthless as teachers. Yet in our field we promote these intellectual midgets.

Edsger Dijkstra is an intellectual midget. The summary of 13000 pages of his work ? Mathematicians are above average, programmers are below average. The whole greatness of "mutual exclusion" is something 2 year olds can come up with. His obssessive compulsive disorder meant that he did not even use computers his entire life, but some fountain pen, everyday. How cool and normal! Edsger Dijkstra did not write 1 usable program in his entire life. 0 operating systems. 0 games. 0 apps. 0 batch processing systems worth a damn. Much like the fake and dysfunctional programmers here in this and in every other forum he hated people who did. If chemists, electronic engineers, mechanical engineers, civil engineers, architects don't need permission from mathematicians and Dijkstra, then programmers don't need it either.

Algol, Dijkstra's brainchild was largely a total and complete failure. 0 usable programs written in algol. ABAP / Cobol is a better language than haskell, lisp, smalltalk and java. Bite me. Don't like it ? Compete in the marketplace. Fund 1000 smalltalk, haskell and lisp startups than ruby startups to make your money, hypocrites. Even after receiving education from the most elitist schools and having VCs who share your grand views on programming, if you still can't run a business with haskell (algol++) and lisp stop wasting everyone else's time, alright ? We are happy with matlab and php.

"GOTO Considered Harmful" Considered Harmful - https://web.archive.org/web/20090320002214/http://www.ecn.pu...

Re: A commemoration of Edsger Dijkstra [pdf]

#27

Post by guicho271828 »

doesnotexist wrote: post #14

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 f…

I actually prefers pens than pencils but with different reasons. With pencils you are tempted to erase things. However, it is an illusion; Eraser does not really erase things, ending up in a dirty paper. It also takes much more time. With pens, erasing is effortless and does not require additional decision to make: Just strikethrough it. Then throw it away when you feel you want to start over.
Post reply on HN