Comment by odyssey7

Programs are already proofs. A 15,000-line proof is going to have a mistake somewhere.

In mathematics, the proofs tend to be resilient to minor errors and omissions, because the important part is that the ideas are correct.

In applied cryptography, errors and omissions are foundations for exploits.

Verifying that those 15,000 lines do what they do doesn't give me much more confidence than thorough unit testing would.