Hacker News new | ask | show | jobs
by ctmnt 59 days ago
Hi Kiran, thanks for following up. FWIW, I enjoy your blog and your work. And I do think it was a valuable bug you found; also nice to see how quickly Henrik fixed it.

Say more about people running Lean in production. I haven’t run into any. I know of examples of people using Lean to help verify other code (Cedar and Aeneas being the most prominent examples), but not the actual runtime being employed.

I took a quick scan of lean-lang.org just now, and, other than the two examples I mentioned, didn’t see a single reference to anything other than proving math.

I’m sure you’re in the Lean Zulup, based on what you’ve been up to. Are you seeing people talk about anything other than math? I’m not, but maybe I’m missing it.
1 comments
gopiandcode 58 days ago
Yes, here's a concrete example: https://github.com/leanprover/SampCert This is an implementation of a verified sampler, in lean. Not an embedding in some other language. The implementation itself is in lean, and a python ffi is used to call into the verified implementation. I don't know if AWS is big enough for your standards, but here is at least one example. Besides that, I'm more reporting on the general vibe I have observed from numerous talks at AI4maths workshops at Neurips, at the DARPA AI4Math ExpMath kickoff, etc. People are considering Lean as a serious programming language. Maybe that's surprising to the mathematicians, but as a PL person, I find the language really nicely designed and I can understand why people want to write in it.
link
ctmnt 58 days ago
You’re right, I should have been more careful in my reference to AWS. No need to be snarky about it.

Let me rephrase: aside from that one example from a couple years ago, I haven’t seen any examples of production code written in Lean. I’d be very interested in being proven wrong, this isn’t something I desire, just what I’ve observed. Have you seen any others?

More generally, you implicitly make a good point: writing important libraries in Lean and calling in from another language is probably the most likely use case. So not programs / apps / binaries written in Lean, but small critical components.

link