note: what follows is a reflection on my own limitations, not Pierce's or the book's. I found working my way through it tough going. I'm not a natural mathema

note: what follows is a reflection on my own limitations, not Pierce's or the book's. I found working my way through it tough going. I'm not a natural mathematician, and found the "formalisation first" approach quite difficult to deal with. I would definitely have found it easier if each type judgement (formula) had a natural language description to go with it: intuition to complement the formality. The code helped in that regard. That's a comment I have with many mathematical / formal texts. I wish authors would write down, in natural language, what they 'hear' in their heads when they read an equation on the page. Some at least have a reference (e.g. "read an upside down 'A' as 'forall'"). (I know it's more nuanced than that: someone experienced with type judgements won't interpret them literally. But even still, they could 'read out' what they see on the page). Having said all that: I did find the book helpful and insightful. Just quite difficult to parse and assimilate the formal content. It certainly gave me a much better appreciation of type systems.