Neil Mitchell is a well-known Haskell expert, so I'm sure he would have used the available tools (if they were useful in the problem at hand). When reasoning a

Neil Mitchell is a well-known Haskell expert, so I'm sure he would have used the available tools (if they were useful in the problem at hand). When reasoning about Haskell code, due to non-strict evaluation you get a kind of "spooky action at a distance." If your program flow is something like "let result = C(B(A())", where A, B, and C are functions, an expression deep within function A may not be evaluated until you are in the middle of evaluating C -- or possibly never evaluated at all, if the value of that A expression isn't required to compute the return value of C. To reason about the runtime behaviour inside A, you may have to reason about the expressions that consume the return value of A. This can feel like chaos to someone who works with imperative languages, and who is used to nice things like explicit, linear stack traces: in Haskell, evaluation is driven by need, not by imperative instruction, and so the execution flow can look inside-out at times. That's not to say that better tooling isn't possible -- but it is a challenging problem.