What I like most about Pierce's book is that he introduces each concept with a formal, abstract definition, complete with proofs of correctness, but also follows that up with a concrete implementation in OCaml. The latter is very easy to follow if you've had some experience with the ML family of languages. I sometimes find myself skipping ahead to the OCaml version when I get lost in the math syntax, which for me is less familiar. I'm planning to come back to Harper's book later, but Pierce's book is the perfect fit for where I am now.
My only criticism is that some parts are very dated given it hasn't been updated in almost 20 years. In particular, the version of Java he discusses throughout the book (pre-generics, pre-type-inference) bears little resemblance to the modern one. And since 2002 we've seen affine types (e.g. Rust) start to have mainstream influence, among other things.
In case it's helpful, I'm compiling a list of resources as I learn type systems, logic, category theory, etc.:
https://gist.github.com/dicej/d1117e5d65155d750c16234e6eff16...