Modern software engineering recognizes a broad range of formal methods for helping ensure that a system behaves correctly with respect to some specification, implicit or explicit, of its desired behavior. On one end of the spectrum are powerful frameworks such as Hoare logic, algebraic specification languages, modal logics, and denotational semantics. These can be used to express very general correctness properties but are often cumbersome to use and demand a good deal of sophistication on the part of programmers. At the other end are techniques of much more modest power — modest enough that automatic checkers can be built into compilers, linkers, or program analyzers and thus be applied even by programmers unfamiliar with the underlying theories. One well-known instance of this sort of lightweight formal methods is model checkers , tools that search for errors in finite-state systems such as chip designs or communication protocols. Another that is growing in popularity is run-time monitoring , a collection of techniques that allow a system to detect, dynamically, when one of its components is not behaving according to specification. But by far the most popular and best established lightweight formal methods are type systems , the central focus of this book.

现代软件工程识别出一系列涉及面很广（broad range）的形式方法（ formal methods ）用以帮助保证系统按照规范（或详细规格）能按照预期的目的正确地运行。在涉及面的一端是强大的框架，像Hoare 逻辑、代数规范语言、模型逻辑和形式语义学。这些形式方法可用来表达很通用的正确属性（general correctness properties），但不适合部分程序员使用，因为它们过于复杂了。在涉及面的另一端则是特殊的功能也很小的自动机，小到可以做进编译器、链接器或程 序分析器。这种轻量的形式方法的一个有名例子就是模型检查器（ model checkers ），一 种搜查有限状态机（如芯片设计或通讯协议）错误的工具。运行时检测（监控）则是另一种越来越流行的模型检查器。它是由一组功能的结合，能够动态地发现系统 的组件不按规范作业。不过，到目前为止最流行最常用的轻量的形式方法却是（编程语言的）类型系统，类型系统也是本书的中心。

As with many terms shared by large communities, it is difficult to define "type system" in a way that covers its informal usage by programming language designers and implementors but is still specific enough to have any bite. One plausible definition is this:

A type system is a tractable （易驾驭的） syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute .

will be rejected as ill-typed, even if it happens that the <complex test> will always evaluate to true , because a static analysis cannot determine that this is the case. The tension between conservativity and expressiveness is a fundamental fact of life in the design of type systems. The desire to allow more programs to be typed — by assigning more accurate types to their parts — is the main force driving research in the field.

静态意味保守：尽管类型系统能够很明确不存在有坏的程序行为，但是由于它不能保证所有情况，所以一些在运行良好的程序行为也会被类型系统拒绝。比如，像程序：
if <complex test> then 5 else <type error>
会被认为是坏类型而被拒绝，虽然 <complex test>永远都是“真”。因为静态分析不能判断 <complex test>永远是“真”这一事实。保守性与表达能力之间的张力是类型系统设计所面临的基本问题。为了尽量的使用程序类型化（通过给程序的各个部分一个精确的类型）是这一研究领域的主要动力。

A related point is that the relatively straightforward analyses embodied in most type systems are not capable of proscribing（禁止; 放逐; 排斥） arbitrary undesired program behaviors; they can only guarantee that well-typed programs are free from certain kinds of misbehavior. For example, most type systems can check statically that the arguments to primitive arithmetic operations are always numbers, that the receiver object in a method invocation always provides the requested method, etc., but not that the second argument to the division operation is non-zero, or that array accesses are always within bounds.

但问题是，大多数类型系统里内置的相对简单的分析没能力禁止那些恣意的程序行为；它们只保证类型良好的程序不会有某些特定性质的非法行为。比如，大部分类型系统可以检测出算术运算操作的操作数是否都是数值……但不能检测诸如被除数是否为零、数组访问是否越界等。

The bad behaviors that can be eliminated by the type system in a given language are often called run-time type errors . It is important to keep in mind that this set of behaviors is a per-language choice: although there is substantial overlap between the behaviors considered to be run-time type errors in different languages, in principle each type system comes with a definition of the behaviors it aims to prevent. The safety (or soundness ) of each type system must be judged with respect to its own set of run-time errors.

能被语言的类型系统去除的坏程序行为常被称为运行时类型错误（run-time type errors）。这里必须注意的是这些运行时类型错误是由语言本身性质决定的（当然不同的语言的类型系统所面向的运行时错误会有重叠的部分），从某种意思上看，类型系统的设计就是为避免某些运行时错误的发生。一种语言的安全性体现在其类型系统对运行时错误的可控制性上。

The sorts of bad behaviors detected by type analysis are not restricted to low-level faults like invoking non-existent methods: type systems are also used to enforce higher-level modularity properties and to protect the integrity of user-defined abstractions . Violations of information hiding, such as directly accessing the fields of a data value whose representation is supposed to be abstract, are run-time type errors in exactly the same way as, for example, treating an integer as a pointer and using it to crash the machine.

类型系统能发现的坏程序行为不仅仅于一些低级错误，像调用一个不存在的函数，类型系统也可以检查高级的（代码）模块性来保证抽象机制的实施。一些违反信息隐藏的行为，像直接访问被抽象过的数据字段，会像其它运行时类型错误那样当掉运行的程序，比如把一个整数当成指针用。

（类型系统）的类型检测自动机常常被内建入编译器或链接器，这也意味着类型检测会自动进行（并且是易控制的在可接受的时间内完成的），不需要人工干预。不过，类型检测在别的地方还存在很多需要程序员参与的空间，比如显式的给程序标注（annotations）类型。这种标注通常都很少量的，为了让程序更易写易读。从原理上讲，通过给类型标注可以实现给程序作全面的形式证明，证明其符合规范。这种情况下，类型检测自动机完全变成了证明检查器……FIXME