Can programming be liberated from the von Neumann style? by John Backus

Our thirty year old belief that there is only one kind of computer is the basis of our belief that there is only one kind of programming language, the conventional–von Neumann–language.

Proofs about programs use the language of logic, not the language of programming.