[nmrm]

> when I program Haskell, Agda, Isabelle/HOL, or Coq.

That's fair. Although Haskell is a bit of an odd man out in that list, both in terms of its nature and in terms of its typical use case.

> That being said, depending on what sort of functional programming you're doing, a strong background in category theory or meta-programming can enabling (or not).

This is where the analogy between the two books breaks down. When you're using a functional programming language as a proof assistant, category theory can be helpful. But this is far less common than meta-programming.

edit: 2nd paragraph.