News for hackers. Stuff that matters.

A comment on A formalization of category theory in Coq. Parent comment

Re:A formalization of category theory in Coq by solomatov on Saturday August 05, 2017 @12:21AM (#14934210)
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.
[ Parent | on HN ]
Re:A formalization of category theory in Coq by cmrx64 on Saturday August 05, 2017 @12:32AM (#14934239)
Lean hits a really good middle ground I think. More resources for Agda probably. But I'm very fond of lean ;)
[ Parent | on HN ]
Re:A formalization of category theory in Coq by solomatov on Saturday August 05, 2017 @12:35AM (#14934252)
Lean 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.
[ Parent | on HN ]
Re:A formalization of category theory in Coq by evincarofautumn on Saturday August 05, 2017 @02:45AM (#14934514)
I 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.
[ Parent | on HN ]