Comment by embedding-shape
2 days ago
> The secret of Lean4 is that its actually a great programming language
Kind of feels like you have to specify for what here, as no programming language is just "great at everything", they all have their places (except Clojure and children which is great at everything obviously). Say I run shell commands, obviously a PL based around proofs will be way too much, compared to if I want to create aircraft stabilizer with movable control surfaces.
I would consider using it on any greenfield personal project where I would ordinarily use Haskell.