Probably, from what people are telling me. But Coq is not a general purpose language, it is a dedicated theorem prover. I don't use Lean as a theorem prover for code (only for mathematics) and I myself don't do any code formalization unless someone offers to pay me.

The reason I code in Lean is because I find it fun, and I think it is a very nice general purpose language; for instance, I like Lean much better than Haskell. If Lean ever gets the libraries Haskell has, I will be really excited.

I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?

I prefer Lean to Haskell (never said Lean is a better language) for fairly shallow reasons really:

- I like Lean's inductive type system much better that Haskell's,

- I prefer eager evaluation by default,

- I like the syntax better,

- I like dependent types; they are dangerous, but it is great to have the option.

I suspect some people may also prefer Lean's macro system to Haskell's, but I haven't worked much with either, so I don't know about that.

Out of curiosity, have you tried Idris? It would tick at least boxes 2 and 4, while possibly being a little bit more geared towards general programming.