Hacker News Reader

> obviously no one’s running any compiled Lean code in any kind of production hot path

Ignorant question: why not? Is there an unacceptable performance penalty? And what's the recommended way in that case to make use of proven Lean code in production that keeps the same guarantees?

View on HN

Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.

Where are you coming up with this from? This is awfully confident for a fact you seem to have conjured up without evidence. As far as I am aware, Lean is interested in being used as a programming language (see: https://lean-lang.org/functional_programming_in_lean/) and people are deploying Lean in production: https://docs.aws.amazon.com/clean-rooms/latest/userguide/dif...

You’re right, there is that one example. Feels like we’re in exception that proves the rule territory. But I’d be very interested in being proven wrong! This isn’t a desire of mine, just what I’ve seen. Do you have other examples?

Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.

Reply on news.ycombinator.com