Dijkstra's review of Backus's FP Turing Award speech
cs.utexas.edu
cs.utexas.edu
The first impression that his functional programming style invites implementations with a lot of concurrency should be complemented by the remark that it invites a lot of traffic that the von Neumann machine doesn't need.
He presents the proving of the correctness of programs as an activity reserved for geniuses: "The complexity of this axiomatic game of proving facts about von Neumann programs makes the successes of its practitioners all the more admirable. Their success rests on two factors in addition to their ingenuity".
And then comes his fundamental complaint "In any case, proofs about programs use the language of logic, not the language of programs. Proofs talk about programs but cannot involve them directly [? EWD] since the axioms of von Neumann languages are so unusable." and he presents as an advantage --without questioning-- that in his system "Algebraic transformations and proofs use the language of the programs themselves, rather than the language of logic, which talks about programs." I am not quite sure what is meant by talking proofs and talking logic. But whereas machines must be able to execute programs (without understanding them), people must be able to understand them (without executing them). These two activities are so utterly disconnected --the one can take place without the other-- that I fail to see the claimed advantage of being so "monolingual".
http://www.stanford.edu/class/cs242/readings/backus.pdf
AFAIR Backus says that C and Pascal are too low-level to be good at problem solving, but pure functional programs, point-free style and a more math-like notation may make programming less error-prone.
"In short, [Backus's lecture] is a progress report on a valid research effort but suffers badly from aggressive overselling of its significance, long before convincing results have been reached. This is the more regrettable as it has been published by way of Turing Award Lecture."