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.
> A 15,000-line proof is going to have a mistake somewhere.
If this proof is formal, than it is not going to. That is why writing formal proofs is such a PITA, you actually have to specify every little detail, or it doesn't work at all.
> Verifying that those 15,000 lines do what they do doesn't give me much more confidence than thorough unit testing would.
It actually does. Programs written in statically typed languages (with reasonably strong type systems) empirically have less errors than the ones written in dynamically typed languages. Formal verification as done by F* is like static typing on (a lot of) steroids. And HACL has unit tests among other things.