Rendered at 04:18:11 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
rstuart4133 4 hours ago [-]
The takeaway quote from the article is:
> The Lean library isn't just tested and validated, it's proved correct. This allows us to let AIs loose optimizing the code, requiring that they update the proof whenever the implementation materially changes.
To me it's a "that's obvious in hindsight, so why didn't I think of it?" thing.
If you can write a zlib compressor in it, you can write anything in it - so this is a technique that could be applied all problems amenable to formal proofs. Formal proofs are almost never worth the cost when they only prove the absence of bugs. Adding another payback, "you get speed as well", alters that equation.
Definitely merits more than 2 points after 20 hours. It feels like some readers can't look past an LLM being involved.
zahlman 1 days ago [-]
> libdeflate unsurprisingly blows it out of the water (unsurprisingly because this is a very carefully tuned implementation using architecture-specific SIMD, that we can't touch in Lean).
... But Rust presumably could if someone did the work?
zahlman 10 hours ago [-]
(I have showdead on, but I'm not going to vouch for your reply.
> The Lean library isn't just tested and validated, it's proved correct. This allows us to let AIs loose optimizing the code, requiring that they update the proof whenever the implementation materially changes.
To me it's a "that's obvious in hindsight, so why didn't I think of it?" thing.
If you can write a zlib compressor in it, you can write anything in it - so this is a technique that could be applied all problems amenable to formal proofs. Formal proofs are almost never worth the cost when they only prove the absence of bugs. Adding another payback, "you get speed as well", alters that equation.
Definitely merits more than 2 points after 20 hours. It feels like some readers can't look past an LLM being involved.
... But Rust presumably could if someone did the work?
https://news.ycombinator.com/newsguidelines.html
> Don't post generated text or AI-edited text. HN is for conversation between humans.
"Signing" your post — which is not the convention here anyway — doesn't make the LLM use any less obvious.)