Types give you positive confidence, unlike tests. But how do you build confidence in the typechecker? By writing test for it...

(Writing a typechecker is a bit like squaring the circle, isn't it?)

An analogy that works for me is via topology. The set of programs that behave in unexpected ways is an open set (and definitely not closed), and the set of programs that typecheck is a clopen set (or at least open). And you pray that their intersection is empty.

I feel like I need a meta/dual topology here ... "the intersection of two open sets is empty?" is NOT open, it is closed, because you can only demonstrate a counterexample. Unless you fix a model, but then the problem shifts to how well your model approximates reality.

Basically, there's no escape from tests. If you want formal truth, you are not dealing with computers as they actually exist. OTOH, types are a way to transfer test confidence from one program (the typechecker) to another (your program).

This gets at a big cultural divide. Most software practicioners care about running programs on actual hardware. A lot of academic type theory is about formal math. I don't think these goals have much in common.

(Which is not to say that either of these goals are bad, just to say that they are different and require different mindsets and (usually) different tools. Obviously I'm biased towards the former. Writing software is my goal and it influences my perspective.)