[bbeonx]

This isn't really a metric. It's a description to help the reader understand the magnitude of effort that went into this project. SLoC is a bad metric for plenty of things, but I think it's fine for quickly conveying the scope of a project to a blog reader.

[odyssey7]

Lines of code is also a poor indicator for “magnitude of effort.”

Tangent: generally I’m more inclined to believe quality is improved when someone claims 1000s of lines reduced rather than 1000s of lines written.

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

[chaitimes]

From my experience, pre LLMs, it was a valid proxy metric for effort

[xeromal]

See: AI generating 1000s of lines

[lionkor]

It's a metric of complexity