July 3, 2013
Have read widely in the area, but while I'm very strong on the philosophical motivation side, I'm very weak on the operational side. Am facinated by perspectives of Lawvere, Lambek and others' perspectives on math & logic. I think I get some of Crole's book, but Jacobs almost completely loses me. Would really like to understand HTT, but it's even further over my head.
Again, my literary familiarity is way ahead of my comprehension, but reflection on programming experience helps a bit in this case. Have worked through part of Pierce's Software Foundations in Coq, played a bit with Agda tutorials, and attended intensive workshops at OPLSS12 last year. Have been making repeated passes through Harper's Practical Foundations book. With a fair amount of hand-waving, am applying a sort of type theory based approach to software specification in my job. (We have some very good candidates for some kind of implementation of dependent types there.) I have always seen programming in terms of mathematical reasoning, so was enthralled to discover propositions as types via the Lambek & Scott book some years ago.
Repeating pattern here - read four dozen books before writing a line of code! Since then, completed Odersky's Scala course on Coursera. Have done elementary exercises in Coq, and played a bit with Agda, Haskell, Ocaml, and F#. Didn't discover true FP until a few years ago, but have written in a weakly functional style in imperative languages since the 80s, because it just seemed like the right thing to do. Have also worked intensively with functional dependencies, normalization, and design for compositional reasoning in databases since the 80s.
FP, types, and categories enthusiast