(0) To view programs as proofs, you need to first view programming languages as logics. Alas, when (or even if!) you view any general-purpose programming langua

(0) To view programs as proofs, you need to first view programming languages as logics. Alas, when (or even if!) you view any general-purpose programming language as a logic, you'll find out that it contains lots of junk theorems that nobody actually wants to consider theorems. (1) Don't conflate “rigorous” with “mechanized”. Rigor is a discipline that rules out invalid reasoning.