Thoughts about types

Types in programming languages define logical properties of a program in that language.

N.B. I am not talking about type annotations, i.e. the programmer may explicitly specifiy types or they may be inferred.

When a program successfully type checks, the execution of the type checker constitutes a proof of those logical properties w.r.t the program (assuming correct, consistent behaviour of the type checker itself).

If a program fails the type checker it implies that (as far as the type checker is concerned) there is ambiguity or logical inconsistency w.r.t to the program (again assuming no bugs in the type checker itself).

Partial functions subvert the type system and therefore undermine the value of the logical proof provided by the type checker. Apparently there is a relationship between this, Turing completeness and the Halting problem, although I don't understand that yet.

One of my goals over the summer is to work through Types and Programming Languages by Benjamin Pierce.