4 ms·
Won't it be easier to teach/use Lean?
by gexaha 4y ago
Won't it be easier to teach/use Lean?
- epgui 4y agoWhy Lean? I know Lean is interesting, but there's also Coq, Idris, Agda... And as others have pointed out, this would probably be a good use case for a lisp too.
- epgui 4y agoUpdate: I just received my copy of the book, and at the bottom of page 4 the authors write: “It would be an interesting endeavour to port the code from Haskell to a language with an even stronger type system, like Agda, Idris or Lean. The authors would welcome contributions in this direction.”
- deterministic 4y agoLEAN/Coq/Idris/Agda allow you to prove mathematical theories out of the box. Lisp not so much. Unless there is a Lisp library that gives you the power of Dependent Types and/or Refinement Types?