|
|
|
|
|
|
by bor0
2872 days 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. |
|
|
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.