>>10
show me one useful program that used formal proofs. Even space shuttle software doesn't use formal testing and no one ever will because it only applies to proof like programs. The most perfect bugless programs like qmail have no proofs and barely any tests.
In math, proofs are communication, not thought. Papert interviewed the world's best mathematicians and physicists and all but 5 favored intuition and feeling the ideas in their body over syntactic manipulation and analysis.