One of Harper's arguments (the author here) is dogmatic and perhaps compelling from a aesthetic point of view. Let me try not to butcher it too badly in what follows.

He believes a few things that in concert arrive at the idea that typed languages are the only interesting point in the design space thus uncovered.

He begins by first rigorously defining what he means by "type". In particular, it's a piece of information computed statically (i.e. using the syntax of a program alone, nothing of its "runtime") which constrains the eventual values the dynamics must take. A "type-safe" program is thus one where the dynamics correspond to the predictions of the statics—in particular, a program respects its type as it operates and the program "does not get stuck" i.e. does not hit an undefined state.

From here he notes the power of union types, types which are "either" A or B. Given a sufficiently large union type, one which reads "either this or that or this or that" for every possible result value of running a program then you can create a "safe" semantics for any language using this type—every program has this giant union type and every choice of dynamics ends up in this giant union type. He then notes that while this genuinely is "type safe" it's kind of boring. Further, all "dynamically typed" languages inherit this boringness since they expose no "interesting" static structure.

(Even if you dislike the argument above, and there's plenty that might cause someone to dislike it, it's worth noting that this line of thought arrives very smoothly at the concept of "hybrid typing" being explored by things like Typescript and Facebook's Hack.)

One of the primary things you could argue with at this point is that having more sophisticated types is interesting and valuable. To this end Harper focuses on what he calls the "Holy Trinity" of logic, type theory, and category theory. The idea is backed by the Curry-Howard-Lambek correspondence which shows that each of these fields is but an image of the other two. In Harper's (paraphrased) words: you know that something is genuine and lasting if you can show it exists in every branch of the Holy Trinity.

So he declares basically by fiat that things which reflect the Holy Trinity are interesting and things which do not are not. Obviously you can levy many arguments to disagree with him here.

But it's hard to declare that the things discovered in the Holy Trinity are boring. This is where cutting edge research on things like Homotopy Type Theory and general Dependent Types live. This produces compelling arguments to back up why "null pointers are a billion dollar mistake" [0] or why if-branching and booleans lack meaningful providence [1]. These ideas, even if they are stripped of their Ivory Tower gleam, are what are slowly percolating into mainstream languages with names like "Enum"++ in Swift and "Optional" in Java.

---

Generally, to finally provide my personal take, I think that Harper is dead right so long as you consider programming languages to be "means of expression". I think that's an interesting POV on languages generally and it's not totally at odds with the more everyday POV that languages are "tools for creation". But they are sometimes at odds since they place the brunt of what they demand of a language at different places. Ultimately, if Harper's program is successful many years from now we'll all use shadows of whatever futuristic grade of dependently typed language gives us maximal expressiveness while nesting it in an ecosystem of tooling and libraries which aid construction of interesting things. I have no idea if Harper's "one true language" exists, but it does seem like increasingly the world is moving that way... thus Harper's enthusiasm about Swift and Rust.

[0] http://qconlondon.com/london-2009/presentation/Null+Referenc...

[1] http://existentialtype.wordpress.com/2011/03/15/boolean-blin...