Not that interesting. The gist of the blog is this: "I know some code is wrong, and I want to avoid it in production. Code that doesn’t typecheck doesn’t run.

Not that interesting. The gist of the blog is this: "I know some code is wrong, and I want to avoid it in production. Code that doesn’t typecheck doesn’t run. Therefore, I write types so that this code does not typecheck." This reasoning can be seen as instance of "abduction". If you are familiar with Philosophy of Sciences, it is seen as Inference to the Best Explanation. Put simply, if we remove the buzzwords, it is an instance of hypothesis generation. How can one test a hypothesis that adding types will fix a set of bugs? Just by adding types, of course. In Philosophy, there is another discussion between types and tokens. This is a variation of the problem of universals. The answer depends on one's ontological commitments, which depends on whether one subscribes to nominalism or to realism, etc.