3 ms·

Lines of code is a pretty poor measurement. Doubly so when you're boasting a large number in the context of cryptographic code.

daquisu 1y ago
Which better measurement do you propose?
bbstats 1y ago
the 2nd sentence: "As of last week, this issue is now closed, and every single hash and HMAC algorithm exposed by default in Python is now provided by HACL*, the verified cryptographic library." it's describing coverage.
bbeonx 1y ago
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.
- lionkor 1y ago
  It's a metric of complexity
- odyssey7 1y ago
  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.
  - xeromal 1y ago
    See: AI generating 1000s of lines
  - chaitimes 1y ago
    From my experience, pre LLMs, it was a valid proxy metric for effort
  - tgv 1y ago
    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 1y ago
      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 1y ago
        > 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.
aseipp 1y ago
It isn't boasting about anything, it's a straightforward description of the 2.5 years of effort they went through for this project, and some of the more annoying "production integration" bits.
deleted 1y ago
[deleted]
titaphraz 1y ago
> Lines of code is a pretty poor measurement But let's say at least that it's abused, exploited, perverted and a molested measurement before we call it a poor one. It not all that bad when you have context.

daquisu 1y ago

Which better measurement do you propose?

bbstats 1y ago

the 2nd sentence: "As of last week, this issue is now closed, and every single hash and HMAC algorithm exposed by default in Python is now provided by HACL*, the verified cryptographic library." it's describing coverage.

bbeonx 1y ago

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.

lionkor 1y ago
It's a metric of complexity
odyssey7 1y ago
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.
- xeromal 1y ago
  See: AI generating 1000s of lines
- chaitimes 1y ago
  From my experience, pre LLMs, it was a valid proxy metric for effort
- tgv 1y ago
  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 1y ago
    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 1y ago
      > 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.

aseipp 1y ago

It isn't boasting about anything, it's a straightforward description of the 2.5 years of effort they went through for this project, and some of the more annoying "production integration" bits.

deleted 1y ago

[deleted]

titaphraz 1y ago

> Lines of code is a pretty poor measurement But let's say at least that it's abused, exploited, perverted and a molested measurement before we call it a poor one. It not all that bad when you have context.