4 ms·
To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples. I try to break this barrier a bit with my upcoming book: Gentl
by bor0 8y ago
To me, personally, the biggest barrier was lack of a proper introduction with a lot of examples.
I try to break this barrier a bit with my upcoming book: Gentle Introduction to Dependent Types with Idris.
I am very interested in this area but it is impossible for newcomers to get a grasp of it without too much digging. Logical Foundations was OK but I was still missing the theoretical explanation ("why does this tactic work? it is magic!").
So with accumulated knowledge from IRC, forums I hope to address this.
- jacoblambda 8y agoOoh I'll check this book out once I get through the pile of stuff I have right now. And as you noted there definitely is a lot of "magic" when it comes to the inner workings of theorem proving tactics. I'm slowly figuring all of that out but like you said it definitely takes time and digging at the moment.
- hackermailman 8y agoThe Little Typer is out soon too https://mitpress.mit.edu/books/little-typer https://mitpress.mit.edu/books/little-typer