4 ms·
Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.
by ctmnt 6mo ago
Yes, 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.