News for hackers. Stuff that matters.

A comment on Lean proved this program correct; then I found a bug. Parent comment

Re:Lean proved this program correct; then I found a bug by tpoacher on Tuesday April 14, 2026 @01:55AM (#47761761)
You're technically right, but what things are versus how they're promoted or understood by most people (rightfully or not) often diverges, and therefore such "grounding" articles are useful, even if the wording addresses the perceived rather than the factual reality.

By way of analogy, if there was an article saying "I bought a 1Tb drive and it only came with 0.91 terabits", I think if you started explaining that technically the problem is the confusion between SI vs binary units and the title should really be "I bought a 0.91 terabit drive and was disappointed it didn't have more capacity", technically you'd be right, but people would rightfully eyeroll at you.

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by danparsonson on Tuesday April 14, 2026 @03:39AM (#47762503)
To be clear, I think the article was fine and the author did some useful work (finding a bug in the runtime of a supposedly provably correct system is indeed a valuable contribution!). I don't agree that it's pedantic to explain why the title feels like a bait-and-switch (and thus does a disservice to the article itself). It's just a bit of feedback for future reference.

I take some comfort from being technically correct though; it's widely accepted by all of us pedants that that is the best kind of correct ;-)

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by tpoacher on Wednesday April 15, 2026 @02:09AM (#47775285)
Weeeellll, teeeechnically, I didn't say "technically correct", I said "technically right".

(just kidding xD)

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by danparsonson on Wednesday April 15, 2026 @03:16AM (#47775705)
Haha dammit - I'll lose my membership at this rate
[ Parent | on HN ]