The argument is that agda is relatively straightforward for haskellers and similarly, coq for ocaml devs to adopt. This is a good succinct example of former.

The argument is that agda is relatively straightforward for haskellers and similarly, coq for ocaml devs to adopt. This is a good succinct example of former. Coq has lots of tutorials http://www.cs.uu.nl/education/scripties/pdf.php?SID=INF/SCR-2011-062 http://www.cs.uu.nl/education/scripties/pdf.php?SID=INF/SCR-... There's also typed racket, which i don't know anything, it's been mentioned to me as "theorems for free" http://docs.racket-lang.org/ts-guide/ http://docs.racket-lang.org/ts-guide/