Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
There are a lot of resources to learn from, and it's hard to pick just one. Below are links to learning about dependently typed programming. I think that the most comfortable path is to learn DT programming first, and then learn more of the pure math and type theory behind it along the way as you get more experienced.
Basically, Coq is the most mature and oldest, but is more tedious to do dependently typed programming with.
Agda is not as mature, but it supports dependently typed programming very well.
Idris is an even newer language that also supports dependently typed programming well, and IMO has the best chance of being a practically used language.
Personally, I mostly use Agda.
Software foundations -
Certified programming with dependent types -
Dependently typed programming in Agda (Agda tutorial) -
The power of pi -
Idris tutorial -
Idris course (4 videos and slides) -
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment