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-...

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/