3 ms·
> 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
by dbdr 6mo ago
> 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?
- ctmnt 6mo agoYes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.
- gopiandcode 6mo agoWhere 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/ https://lean-lang.org/functional_programming_in_lean/) and people are deploying Lean in production: https://docs.aws.amazon.com/clean-rooms/latest/userguide/differential-privacy.html#dp-overview https://docs.aws.amazon.com/clean-rooms/latest/userguide/dif...
- ctmnt 6mo agoYou’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.