水木的FuncProgram上最近为这个问题引发了一场大水（其实也不大，在那个版上算比较大了 XD），里面有一个很不错的引用，现摘录如下：

Type theorists' view: It's about primitives.

Type safety is not directly related to memory.  If you read the literatures in the research of programming language type systems, you will find little explicit mentioning of memory concerns, unless the paper is explicit addressing memory management.

For a language to be interesting, there must be some pre-defined primitives values/functions.  This is parallel to mathematical induction, where you must have base cases/axioms.  Programming is really just a way to synthesize such primitives using combinators to form composites of more complicated functionalities.  For instance, usually a general purpose language will provide arithmatic operations, such as “+”.  ”+” takes two numbers as inputs and generate a number as output.  Note that “+” will only work appropriately if provided two numbers.  If the inputs are not numbers, “+” will not make sense and will malfunction.  With this understanding in mind, here come types:

Classic type systems assure one thing: at run-time, all the primitives will be guaranteed to function appropriately, i.e., you will NOT get a type error at run-time.

For instance, if a program is well-typed, then by whatever complicated way you use the function “+”, the inputs to it are guaranteed to be two numbers, and there is absolutely no way for it to malfunction in any possible run-time trace.

Programmers' view: It's about memory interpretation.

In programmers’ eyes, primitives correpond to language built-in functions. For instance, the “printf” funcition in C, the “bind” function in Haskell. These functions correspond to code stored as bits in memory code segments. When executed, they operate on some certain data, which is also stored as bits in memory data segments.  In such operations, the function needs to interpret the bits in some certain ways, because usually the bits do not interpret themselves (in common statically typed langauges).  For instance, the function “+” will interprets its first argument (represented by some bits) as a number.

From this point of view, what type systems assure is truly the correctness of memory interpretation, that is, if some bits are to be interpreted by the run-time system as a number, then these bits truly represents a number but not a string or a pointer to a linked list.

In fact, it is very hard for a type system to assure the consistency of memory access in a language with explicit memory manipulation such as C. There are many proposals on how to prevent accessing dangling pointers in such languages, but they are either too restricted or too complicated to be practical.