3 ms·
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 intere
by gopiandcode 6mo ago
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/ 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.