[pertymcpert]

I really don't think they have an axe to grind. What do they say that's incorrect? Their point is that much of what we see as type theory is inaccessible to the average programmer.

When we say that some field is inaccessible, we don't blame the reader trying to understand. At the same time we're not saying that the field is wrong either, but that communication could be improved.