In most of your statically-typed OOP languages, a type declaration really is just an assertion like "the value bound to 'foo' is always a number". This falls far short of asserting that it has the intended properties. For example, "is a number" is miles away from "is the largest prime number less than n."

For most interesting programs, it is simply not enough to have something which is a number. So you must use some supplementary mechanism to verify all the interesting properties. In practice the supplementary mechanism is not as awkward as writing extended type theory proofs in your programs. Now if this supplementary mechanism is good enough to depend on for all the interesting correctness checks, why isn't it good enough for the basic stuff as well?

If you do make the type system expressive enough to verify everything, it is Turing complete, and many assertions are only verified by calculating them in the type system. But if you write a correct implementation in your Turing-complete type system, it is at least as easy to write a correct implementation in the ordinary way. So why not just write the same code twice, and raise an exception if a result does not get a quorum?

This might be a valid strategy for some cases. But in most cases, some kinds of errors are just much more important to cover than others.

Static vs. dynamic typing is not the issue. The first issue is what kind of system you have for annotating code with appropriate assertions - easier is better, assuming that more assertions are always better.

The second issue is how much of this annotation is mandatory. Push it to the limit and you get a "bondage and discipline" language. Pair it with a type system that is less than extraordinary and you spend a significant share of your time wrestling an awkward type system.

Some people seem to enjoy this activity. But unless you do most of your coding under the influence of heavy sedatives, the odds are that the majority of your errors are not simply passing the wrong primitive type. And unless something is really wrong with you, most of your errors are not due to your inability to put an unbreakable padlock on your own code to limit your own intentional malice. So it is certainly possible to emphasize these cases.

But that should be based on some understanding of costs. If a given class of error is infrequent and low-cost, there should be a burden to justify spending 50% more time always handling that class of error.

If the language understands those costs better than the human then that could be helpful (particularly applicable to DSLs). But if it does not then it is better for the human to be able to manage this for themselves.

The real argument seems to be about which classes of assertions should be mandatory, not anything about the internal type accounting. Seems to me that this should be a decision specific to the purpose. If you are teaching programming your requirements might be different from if you are writing missile guidance systems. Moreover, different people might have different tastes!

So I am getting pretty tired of the facile suggestion that static typing (in particular, as implemented in mainstream blub languages) is invariably safer and that this makes it an obvious choice. The only variable at hand is NOT how much you care about maintaining invariants. It is really not that simple. It is also very significant what kinds of invariants you mean to maintain and what amount of cost you are willing to absorb to maintain them.