I agree. Programming is an applied form of constructive logic. A program that works is an example (existence proof) that its specification (a theorem) can be fulfilled (proven). When we review code, we’re generally trying to disprove—looking for ways in which the program <i>doesn’t</i> fulfill the specification.