4 ms·
To really learn coq, you need to learn type theory which is hidden behind tactics. IMO, Coq isn't the best way to do so. I highly recommend starting with Agda i
by solomatov 9y ago
To really learn coq, you need to learn type theory which is hidden behind tactics. IMO, Coq isn't the best way to do so. I highly recommend starting with Agda instead.
- cmrx64 9y agoLean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
- solomatov 9y agoLean is very interesting, but Agda and especially Coq has more learning resource, so for the beginners it's probably better to start from them, even though, in some sense Lean is more modern.
- evincarofautumn 9y agoI have the impression that for someone coming from a programming background, Idris is also a pretty good introduction to the world of dependently typed programming and proof assistants.