[bmer]

Full disclosure:

a) Dijkstra is a bit of a personal "hero" of mine (hero in quotation marks, because I don't like to think of myself as a hero worshipper), because it was due to him I learned of textbooks written by guys like Eric Hehner and Roland Backhouse, which ended up changing my life significantly.

b) I do not really grasp the technical issues being discussed in the correspondences between Dijkstra and Backus

Given this disclosure:

Regardless of the cultural issues (which I suspect you are right about), I found Backus' first response to Dijkstra full of ad hominems, and very light on technical rebuttals. If we subtract out the ad hominems, I suspect the technical rebuttals would take less than a page (which is a significant reduction, considering that the full letter is 4 (typewritten!) pages).

Calling Dijkstra arrogant seems to have been a popular insult (as Backus himself admits), so I wonder if Backus was simply jumping onto the bandwagon as a defensive reaction to the arguments presented in EWD 692.

I think Dijkstra's responses were indeed trollish. I wish he wouldn't have said anything further after he noticed the gratuitous personal attacks against his character in Backus' response, but he couldn't help but say something back. Oh well.

Can you comment on this observation?

[c3534l]

I personally found Backus to be way more of a dick in these letters, though I did gloss over some parts. It's strange how different people can get very different things from these letters. Maybe they just didn't have personalities that meshed well. I don't think it's cultural: I'm American and I find Dijkstra's demeanor to be perfectly acceptable, if a little a colorful. Although, in the same vein, people often don't like Linus Torvalds for many of the same reasons.

[tps5]

I found Dijkstra's letters appalling. Writing - utterly without shame - that his negative response to Backus' paper was disingenuous and served a "political" purpose is utterly despicable to me.

I don't know how you can defend that.

[_prototype_]

Dijkstra was very rude

[Bromskloss]

> textbooks written by guys like Eric Hehner and Roland Backhouse

Would you like to say something about those?

[bmer]

E. Hehner has a course called "Formal Methods for Software Design", which he presents completely openly online (including video lectures, a textbook, solutions, and so on): http://www.cs.toronto.edu/~hehner/FMSD/

I really liked it.

I also liked R. Backhouse's approach to it, encapsulated in two books:

1) less playful: http://www.amazon.com/Program-Construction-Calculating-Imple...

2) more playful: http://www.amazon.com/Algorithmic-Problem-Solving-Roland-Bac...

If you are looking for motivation, you might also like: http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

-----------------

I found Dijkstra's stuff to be easier to read after I had read books by Hehner/Backhouse, even though chronologically, Dijkstra came first.

[Cyph0n]

Thank you for linking that course. I've always been interested in formal methods and verification of correctness.

[bmer]

No problem. You'll notice as you go through the links that none are about verification of correctness. Rather, they are about "correct by construction".

[nickpsecurity]

Hehner's work is on my reading list. The reviews on Backhouse's links aren't promising.

[bmer]

I have learned not to put much weight in Amazon reviews for technical literature. Borrow a copy of the books from a library (my city library actually had access to a digital version of Backhouse's latest book, and you could always Yarr! yourself a copy) and check them out, before shelling out the cash :)

[nickpsecurity]

Well, the one reviewer said it was only a start toward a method for practical software with practical part maxing out at a sorting algorithm. Is that true or do you have examples of realistic stuff covered by book?

[bmer]

Backhouse's more playful book, focuses primarily on teaching one how to write and use proofs in the "calculational style" of Dijkstra/Hoare/Lamport/others.

Backhouse's less playful book covers the same topic, but has some more programming examples:

* cyclic code error correction * simple sorting algorithms * real number to integer conversion is used to introduce Galois connections

Again, this isn't a lot in terms of "practical examples". No production level software is built here. If you're looking for that sort of stuff, maybe you want to try out L. Lamport's book: http://www.amazon.com/Specifying-Systems-Language-Hardware-E...

I haven't read that book though.

[vanderZwan]

You're right that the technical rebuttals are fairly slim, but the rest of the exchange, which is all about political play and saving face[0], isn't pointless.

The whole argument Dijkstra makes boils down to "if everyone was as technically competent as you and I, then I wouldn't need to do this. But the sad truth is that the incompetent are not only the majority, they decide what gets funded and researched, so I have to." I think he is right about that, and probably even acted correctly on it, but even so: positioning himself like he's taking on a sacrificial trollish saviour role and just doing this to save programming research is pretty arrogant, so Backus is right as well!

And that's just the politics of it, saving public face hasn't even entered the equation here. Don't forget, Backus' reputation also directly affects the respect and by extension funding that he receives for research that he wants to do. With that in mind I can very easily see how Backus must have been furious after reading EWD692, especially considering that it contained a few insinuations about him, which again I would partially account to Dutch culture, which (used to) have a severe case of tall poppy syndrome[1]. But from Backus' point of view, if they had been friends and colleagues before, it might have felt like backstabbing, both politically and as friends.

So I think I understand Backus' ad hominems - I suspect he was sincere about trying to criticise Dijkstra from the position as a long-time friend; his writing style boiling down to: "Look, I respect you and all, but I have to point out that you're being a dick; oh and have a taste of your own medicine on the side, because two can play that game."

Of course, it looks like he played right into the hands of Dijkstra, because Dijkstra doesn't appear to be as emotionally invested in saving public face, and seems to rather enjoy puzzling Backus a bit longer.

In general, I think it speaks for both of them that they managed to resolve these differences to what appears to be mutual satisfaction!

[0] https://en.wikipedia.org/wiki/Face_(sociological_concept)

[1] https://en.wikipedia.org/wiki/Tall_poppy_syndrome

[Ericson2314]

Hah, I'd say that both Dijkstra and Backus are "heros" for me---scare quotes for the exact same reason. I'm mainly interested in ideology/vision in reading about the early pioneers, and I find theirs more interesting than, let's say, Knuth's.