This seems somewhat of a silly critique. By the same logic, we know that the vast majority of problems can not be solved by any program, yet we write programs t

This seems somewhat of a silly critique. By the same logic, we know that the vast majority of problems can not be solved by any program, yet we write programs to solve problems everyday. Or we know that the vast majority of mathematical statements cannot be proven or disproven, yet we can do math proofs just fine. I think we don't suffer from this because we end up asking questions that are relatively simple. Technically, there are many more uncomputable numbers than computable ones, but we are much more interested in the infinitely smaller set of the computable numbers than the uncomputables. (Furthermore, we are much more interested in rationals than we have any right to be, considering that there are many more real numbers than rationals). There should be a similar premise for type systems. Perhaps any type system will disallow valid statements, but we can try to make it so that those valid statements are above a certain length, say 100,000. Then, there are still infinitely many valid statements that are illegal, and they may be much more elegant than their counterparts, but they're so long that it is irrelevant for practical purposes. Now, actually building a type system like that is a whole 'nother beast. I imagine you would give up some notion of completeness for a level of "predisposition", that is, the type system predisposes programmers to making legal statements in the same way that normal number systems(reals, rationals) predisposes mathematicians to making provable statements. A slight nudge towards writing programs in a certain style can go a long way in terms of avoiding "illegal but valid" statements.