[danite]

I'd say there's also a big difference in the sort of correctness that static types guarantee vs the correctness that tests give you. Tests, to borrow some phrasing from Donald Rumsfeld, are only really effective against "known unknowns" not "unknown unknowns." Tests are only as thorough as the test writer and the "known unknown" cases they can come up with to test against. But as software developers we've all been in the situation where some case that you didn't think to test for is what winds up causing a bug (an "unknown unknown").

Static type systems on the other hand, can give you much greater guarantees of correctness (if they're sound). Due to the Curry-Howard isomorphism we know that programs in sound static type systems are the same as mathematical proofs. That's a much stronger guarantee than what you're given by testing alone. The problem of missing a case in your testing goes away if you have a mathematical proof that that case cannot occur. You've taken away some of the burden of thoroughness from the programmer and given it to the compiler instead.

In a perfect programming utopia we would all encode the desired properties of our programs in static types and have no need for testing because we'd have proofs of correctness. The problem of course is that writing those kinds of proofs into types is very time consuming and tedious and isn't realistic for most software development. So we still need tests to cover what is too expensive or complicated to type.