Chris Smith on type

Chris Smith has a good article on static and dynamic typing. It is clear about the terminological confusion:

I realize that may sound ridiculous; but this theme will recur throughout this article.  Dynamic and static type systems are two completely different things, whose goals happen to partially overlap.

It does overstate the confusion is a few places (weak and strong typing do have widely accepted definitions) but in general it's very good until the last third, when it falls into the very trap it warns about: supposing that all type systems have the single goal of proving correctness. That is not a goal of dynamic typing at all, and it's not even a major goal of static typing for most users, because the properties ordinary type systems prove are rarely the ones programmers care about. The main point of static typing, at least for me, is not to prove anything, but to find bugs. I don't care if the type system proves that a particular bug doesn't exist, because that's rarely information I can use. But when it locates a bug - or even suspects one - that is valuable, because it saves time. Proofs may help find bugs by narrowing the search space, but the proofs themselves are not why we use typecheckers. We use them to find bugs faster.