Both this assertion and the one that types are "a set of compiler-enforced contracts between pieces of code" are very wrong ways of thinking about types, and th

Both this assertion and the one that types are "a set of compiler-enforced contracts between pieces of code" are very wrong ways of thinking about types, and the reason why most statically typed languages are so poorly designed and get such a bad reputation. Static typing in a programming language is a mechanism for making certain types of non-terminating computations impossible to express in that programming language. The understanding "non-terminating" here includes errors as well (the idea of bottom ⊥ that you'll find in some earlier texts on programming languages semantics, such as Allen's Anatomy of Lisp). Non-terminating computations are equivalent to paradoxes in formal logic (see Curry-Howard correspondence), and the first type system was developed to deal with Curry's paradox (http://en.wikipedia.org/wiki/Curry%27s_paradox http://en.wikipedia.org/wiki/Curry%27s_paradox) in the first programming language (lambda calculus). Some type systems prevent more types of non-terminating computations, others less. But saying that run-time type assertions are equivalent to a typed programming language, or that types are like contracts or other things just leads to confusion.