The thing is, though, that you mostly only get errors for code that is actually executed. So, your program is only fully type checked when all code paths are executed. In the case of python one can ameliorate this situation a bit by using mypy. At my job I see very often code being broken because, e.g., the signature of a function was changed but not in all places and so on. Now somebody will say that the IDE can solve that but these colleagues who are regularly breaking the code are actually using IDEs and it somehow still does not help. I have come to think that code that is not compiled and/or otherwise type checked is just not very serious and certainly not worthy of production environments.

> your program is only fully type checked when all code paths are executed.

The solution to this is to make sure that, during testing, all code paths are executed. And that’s something you should be doing anyway, to find bugs that aren’t type errors.

I've worked with Python codebases that had very extensive test suites and I've still encountered many cases of bugs slipping through that a static type check would have caught. Its really hard to make sure tests are fully comprehensive. About the best you could do is generative property-based tests, but then the feedback loop is not great as it may take minutes, hours, days or weeks for a particular problem case to be generated, while the static check would have caught it at compile time or even interactively in your IDE.

I don't hate dynamic languages, but this is a pretty major weak spot for them, in my personal opinion, and one that's bitten me a number of times.

That is impossible with almost all non-trivial software. Testing proves only the presence of errors not their absence.

> Testing proves only the presence of errors not their absence.

I've never thought of it that way, but that totally makes sense.

You can think of the compiler for a statically typed language doing exactly that at runtime for a subset of potential errors -- the type errors. Some people claim that they never make them and they may well be correct. I do commit such errors so compiler is a friend, but a pedantic friend.

I am all for high test coverage. One should not underestimate the effort in that, though. Some time ago I covered some two thousand lines of code completely in tests. As in, all code paths, checking all side effects. Kind of an effort in the spirit of "dealing effectivly with legacy code" by Michael Feathers. They were quite non-trivial and it took me about two months. Doing such a thing may not always be feasible. Also if code is written by others they may have covered fewer code paths in tests than one would have liked. A type checker will check all code paths but the tests that your predecessor failed to write are not checking anything.