> My original reply was to someone who thought proofs are all unit valued That is the danger if you get too married to the idea of proofs as programs, and thin

> My original reply was to someone who thought proofs are all unit valued That is the danger if you get too married to the idea of proofs as programs, and think about it like a programmer, not a mathematician. Listen, if thinking about proofs as programs helps you, great! Personally, I never found it helpful, and it never helped me solve anything.