3 ms·

Lean is a dsl for mathematicians, not computer programmers.

• nylonstrung 2mo ago
  This is not remotely true, it was designed as a general purpose functional programming language and the adoption by mathematicians only came later with the creation of Mathlib. It's not a DSL but has very powerful metaprogramming capabilities that make it great for creating DSLs There's nothing the core language lacks compared to say Haskell
  • IsTom 2mo ago
    I wish DX was better for people not using VS. I have my opinions about tools and when trying lean out I got the impression that you basically have to use it. They also seemingly lack a REPL. I also got the impression that they like sticking everything into Mathlib and not splitting off smaller packages that you could use as dependencies (besides Batteries).
    • nylonstrung 2mo ago
      Yeah I really dislike that you need neovim or VS to benefit from Infoview Haven't tried it but there's this community-made REPL https://github.com/leanprover-community/repl https://github.com/leanprover-community/repl
      • IsTom 2mo ago
        Using JSON as input and output of a REPL is certainly a choice.
• deterministic 1mo ago
  Completely and 100% utterly wrong. LEAN is a functional programming language with a type system strong enough to express cutting-edge mathematics and proving it correct. And yes it also has DSL's built on top of it optimised for doing math but that is an extra.