4 ms·
Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?
by nequo 2y ago
Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?
- ykonstant 2y agoProbably, 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.