The example proofs he gives in the article have nothing to do with the way he taught to do programming, they are merely illustration of some of his minor points. Later in the article he says:
On the other hand, we teach a simple, clean, imperative programming language, with a skip and a multiple assignment as basic statements, with a block structure for local variables, the semicolon as operator for statement composition, a nice alternative construct, a nice repetition and, if so desired, a procedure call. To this we add a minimum of data types, say booleans, integers, characters and strings. The essential thing is that, for whatever we introduce, the corresponding semantics is defined by the proof rules that go with it.
As I read it. His comments about teaching we along the lines of:
1. Thinking of a computer as machine is not helpful. He re-iterates this point on "operational reasoning" in other EWD's when describing inductive thought in understanding programs rather than thinking step-wise.
2. Unsuitability of engineering metaphors / maintenance (such as topping up the oil in an engine) and so on to describe tasks within computer programming.
3. Calling bugs "errors"
4. Avoiding anthropomorphising programs
etc.
The given informal proof is given to argue for "use of down to earth mathematics" as a way of thinking about programming in a way that avoids "tremendous waste of mental effort "seems to be among the core points of this EWD.
The points about Liebniz's dream seem to be referring to the broadening and deepening of the formal core of computer science which was and still is a highly lively and profitable endeavour. And the argument is that making computer science students familiar with formal mathematics and logic can only help the endeavour.
The part you quoted just sounds to me just sounds like a pedagogical computer language. The main thrust seems to be ensuring students have a grounding in logic and formal math. Not to have them necessarily feed all their programs in to formal solvers and expect to do so all their lives. Although predicate transformer semantics was one research effort he led in to exactly that.
He does touch on the presentiment of things like predicate transformer semantics in the EWD but very obliquely as highly speculative statements on future research. I haven't read "discipline of programming" (I'd love to but it's expensive) but it looks like a scientific publication outlining a research program rather than a students handbook. Scientific research always proceeds through what might look like blind alleys in retrospect but which are actually important contributions.
Also from the lectures of his that I've seen, it seems the content is usually more along the lines of the EWD's than formal treatises in to predicate transformers.
Sorry for length of reply but, Dijkstras thinking on these issues, IMO, whatever you think of it, is not easily dismissed.
EDIT: In fact, to me, dismissing dijkstras ideas on formal comp-sci because of predicate transformer logic is like dismissing Newton for thinking that action at a distance was an "absurdity no man could believe in." That is to say, one cannot dismiss Newtons body of work as merely a preamble for his "main work" of finding a way to disprove action at distance.
Comments
The example proofs he gives in the article have nothing to do with the way he taught to do programming, they are merely illustration of some of his minor points. Later in the article he says:
On the other hand, we teach a simple, clean, imperative programming language, with a skip and a multiple assignment as basic statements, with a block structure for local variables, the semicolon as operator for statement composition, a nice alternative construct, a nice repetition and, if so desired, a procedure call. To this we add a minimum of data types, say booleans, integers, characters and strings. The essential thing is that, for whatever we introduce, the corresponding semantics is defined by the proof rules that go with it.
This sounds exactly like a description of:
http://en.wikipedia.org/wiki/Predicate_transformer_semantics
And of the approach he uses in "The discipline of programming", so I think you are the one who is confused.
As I read it. His comments about teaching we along the lines of:
1. Thinking of a computer as machine is not helpful. He re-iterates this point on "operational reasoning" in other EWD's when describing inductive thought in understanding programs rather than thinking step-wise.
2. Unsuitability of engineering metaphors / maintenance (such as topping up the oil in an engine) and so on to describe tasks within computer programming.
3. Calling bugs "errors"
4. Avoiding anthropomorphising programs
etc.
The given informal proof is given to argue for "use of down to earth mathematics" as a way of thinking about programming in a way that avoids "tremendous waste of mental effort "seems to be among the core points of this EWD.
The points about Liebniz's dream seem to be referring to the broadening and deepening of the formal core of computer science which was and still is a highly lively and profitable endeavour. And the argument is that making computer science students familiar with formal mathematics and logic can only help the endeavour.
The part you quoted just sounds to me just sounds like a pedagogical computer language. The main thrust seems to be ensuring students have a grounding in logic and formal math. Not to have them necessarily feed all their programs in to formal solvers and expect to do so all their lives. Although predicate transformer semantics was one research effort he led in to exactly that.
He does touch on the presentiment of things like predicate transformer semantics in the EWD but very obliquely as highly speculative statements on future research. I haven't read "discipline of programming" (I'd love to but it's expensive) but it looks like a scientific publication outlining a research program rather than a students handbook. Scientific research always proceeds through what might look like blind alleys in retrospect but which are actually important contributions.
Also from the lectures of his that I've seen, it seems the content is usually more along the lines of the EWD's than formal treatises in to predicate transformers.
Sorry for length of reply but, Dijkstras thinking on these issues, IMO, whatever you think of it, is not easily dismissed.
EDIT: In fact, to me, dismissing dijkstras ideas on formal comp-sci because of predicate transformer logic is like dismissing Newton for thinking that action at a distance was an "absurdity no man could believe in." That is to say, one cannot dismiss Newtons body of work as merely a preamble for his "main work" of finding a way to disprove action at distance.