on "On the cruelty of really teaching computing science" Dijkstra, in his essay On the cruelty of really teaching computing science, makes the following proposal for an introductory programming course:

On the one hand, we teach what looks like the predicate calculus, but we do it very differently from the philosophers. In order to train the novice programmer in the manipulation of uninterpreted formulae, we teach it more as boolean algebra, familiarizing the student with all algebraic properties of the logical connectives. To further sever the links to intuition, we rename the values {true, false} of the boolean domain as {black, white}.
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.
Right from the beginning, and all through the course, we stress that the programmer's task is not just to write down a program, but that his main task is to give a formal proof that the program he proposes meets the equally formal functional specification. While designing proofs and programs hand in hand, the student gets ample opportunity to perfect his manipulative agility with the predicate calculus. Finally, in order to drive home the message that this introductory programming course is primarily a course in formal mathematics, we see to it that the programming language in question has not been implemented on campus so that students are protected from the temptation to test their programs.

He emphasises that this is a serious proposal, and outlines various possible objections, including that his idea is &quot;utterly unrealistic&quot; and &quot;far too difficult.&quot;

But that kite won't fly either for the postulate has been proven wrong: since the early 80's, such an introductory programming course has successfully been given to hundreds of college freshmen each year. [Because, in my experience, saying this once does not suffice, the previous sentence should be repeated at least another two times.]

Which course is Dijkstra referring to, and is there any other literature available that discusses it?
The essay appeared in 1988 when Dijkstra was at the University of Texas at Austin, which is probably a clue -- they host the Dijkstra archive but it is huge, and I'm particularly interested in hearing from others about this course.
I don't want to discuss whether Dijkstra's idea is good or realistic here. I considered posting this on cstheory.se or cs.se but settled on here because a) a community of educators might be more likely to have someone who can answer easily, and b) Dijkstra himself emphasises that his course is &quot;primarily a course in formal mathematics.&quot;  Feel free to flag for migration if you disagree.
This is pretty much what TU Eindhoven's Computing Science education, designed and implemented by Dijkstra and colleagues, was like from the time it started, around 1980, until Dijkstra's influence started to wane, somewhere half way through the 1990s.

I started studying CS at Nijmegen University in 1982; a classmate did the same at TU Eindhoven. Every spring, our old secondary school would have a day on which former students would introduce their chosen field of study to current students, and we were both there to introduce CS, so we compared our experiences. They were vastly different. In Nijmegen, we obtained actual experience with actual programming languages, actually running our assignment programs on an actual computer (a VM/CMS virtual machine, to be precise). Not so in Eindhoven.  My former classmate told me they weren't allowed to touch a computer in the first year. Programming, in Eindhoven, meant learning to mathematically construct provably correct algorithms from mathematically stated problem definitions.  On paper.

This attitude was somewhat relaxed after Dijkstra left, but even in the early 1990s, the courses called Programmeren (Programming), numbered 1 to 9, and spanning several years, still consisted of that same activity, and one in particular presented a major hurdle for the students. I never took any of those courses, but I doubt any use of computers was involved.

In case you're wondering: today's computer science education at TU Eindhoven is very different.