With deference to Dr Kell, I think this is overwrought. He has some good points, points made happily against a particular form of "type cultist" who oversimpli

With deference to Dr Kell, I think this is overwrought. He has some good points, points made happily against a particular form of "type cultist" who oversimplifies argument toward making types out to be something magical. They're not, no sane person would think so, but they are a static, syntactic proof system pertaining to the meaning of your programs and there's a lot to be said for such technology. I am happy to quibble exact points made in this rant, but I'm on my phone so for now I'll merely say that there's a large design space of programming languages and a similarly large (perhap today larger) space of type theories. Matching them up to hit all of your tradeoffs is hard, but there have been some great successes and I would happily contend that any professional programmer owes it to themselves to explore this design space "in anger". I'm also happy to generally claim that faster, more complete feedback is better than the opposite. Static systems of all regards are faster than "dynamic" ones, and most of them are more complete. This is where you hear about comparisons of types (especially dependent ones) and tests. It's great stuff to think about and explore. Further, I want to emphasize that SMT solvers are fascinating too and nobody thinks that they're not. The style of proof they provide is more expressive and less certain, though, so the right answer is to know how to combine all of these modes of evidence.