4 ms·
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 f
by ykonstant 2y ago
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.
- Tainnor 2y agoI've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?
- ykonstant 2y agoI 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.
- Tainnor 2y agoOut 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.