Why Lean is faster than Rust
kim-em.github.io
Why Lean is faster than Rust
1–5 of 5 posts
Re: Why Lean is faster than Rust
#2> 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?
Re: Why Lean is faster than Rust
#3> 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?
[flagged]
Re: Why Lean is faster than Rust
#4> 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?
(I have showdead on, but I'm not going to vouch for your reply.
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.)
Re: Why Lean is faster than Rust
#5The 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.