[Ericson2314]

IIUC, Backus also talks about correctness proofs with "Von Neumann model" languages just being a lot harder to prove, a separate point from the language for the proof itself. Well, that's a huge selling point for PL research to this day, Dijkstra evidently came fully on board years later as evidenced in https://www.cs.utexas.edu/users/EWD/transcriptions/OtherDocs...:

> A fundamental reason for the preference is that functional programs are much more readily appreciated as mathematical objects than imperative ones, so that you can teach what rigorous reasoning about programs amounts to.