[yw3410]

I don't think this is true (or at least not true for all programs); there's a whole discipline of software which shows how close writing software is to formal logic/inductive proofs in Agda Coq, etc.