[tgv]

Do you remember writing the proof for quicksort, which is say 0.1k lines? 15k lines of verified code is a pretty good indication of effort.

But the problem may come from the headline, which is somewhat clickbaity. HN forbids changing it, and then part of the discussion focuses on the literal content of the headline, which is, as you rightly hint, not the best summary of what's interesting here.

[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.

[the-lazy-guy]

> 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.