By the way, Backus was later of the opinion that programming languages should get even more mathematical (which is not the same as less human.) He explicitly criticizes then extant languages for "their lack of useful mathematical properties for reasoning about programs".
That's the sentiment I expressed that started this whole sub-debate. I said "Not as many people recognize the reverse - the applicability of mathematical techniques to studying computation." (And from there we got to programming language design as an example.) I think Backus would agree.
Of course, he goes much further than a simple surface sentiment. He's thought about it, and saw founding languages even more directly on richer mathematical abstractions (than general formal languages or more restricted CFLs):
"Combining forms can use high level programs to build still higher level ones in a style not possible in conventional languages. Associated with the functional style of programming is an algebra of programs whose variables range over programs and whose operations are combining forms. This algebra can be used to transform programs and to solve equations whose ?unknowns? are programs in much the same way one transforms equations in high school algebra. These transformations are given by algebraic laws and are carried out in the same language in which programs are written. Combining forms are chosen not only for their programming power but also for the power of their associated algebraic laws. General theorems of the algebra give the detailed behavior and termination conditions for large classes of programs." - -- John Backus, 1977 Turing Award Lecture: "Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs"
