1 语言中的类型和框架

    探索意味着有一个目标，发现却意味着目光自由，胸怀坦然，没有目标。
    
    --黑塞

1.1 语言框架

现代软件工程承认应用范围广泛的形式化方法，

以帮助确保系统在某些特定方面正确运行 隐式或明确地表明其期望的行为。

类型系列的一端是强大的框架，例如 数理逻辑、代数规范语言、模态逻辑和指称语义。

这些可以用来表达非常普遍的正确性属性，但通常使用起来很麻烦并要求程序员有大量的复杂性。

1.2 语言技术

在另一端是力量更温和的技术，以至于自动检查器可以内置在编译器、链接器或程序分析器中，

因此即使是不熟悉底层框架的程序员也可以熟练应用理论。

这种轻量级形式方法的一个著名实例是模型检查器，在有限状态机系统中搜索错误的工具，

例如：
    芯片设计
    通信协议

示例，知名协议tcp的一个经典有限状态机：

另一个非常流行的是运行时监控比如runtime，它是一组允许系统运行的技术的集合。

动态检测其组件之一的行为是否符合到规范。

但迄今为止最流行和最成熟的轻量级形式化方法是类型系统，是未来的中心焦点。

类型系统是一种易于处理的句法方法，

用于证明不存在通过根据种类对短语进行分类来确定程序行为他们计算的值。

1.3 类型系统关注点

有几点值得关注。

这个定义标识类型系统作为推理程序的工具。

这一措辞反映了面向编程语言中的类型系统。

更一般地，术语类型系统（或类型理论）指的是逻辑、数学和哲学的研究领域，这是更广泛概念。

类型这种意义上的系统在 1900 年代初期首次正式化，

为了避免出现威胁数学基础的逻辑悖论，例如罗素的理发师悖论 (Russell, 1902)。

在二十世纪，类型已成为逻辑中的标准工具，

尤其是在证明论中（参见 Gandy，1976 年和 Hindley，1997 年），并已渗透到哲学语言和科学。

该领域的主要里程碑包括：

   罗素的原始类型理论（Whitehead 和 Russell，1910）、
   拉姆齐的简单类型理论(1925)
   Church 的简单类型 lambda 演算的基础 (1940)
   Martin Löf 的构造类型理论 (1973, 1984)
   Berardi、Terlouw 和 Baren dregt 的纯类型系统 
   (Berardi, 1988; Terlouw, 1989;巴伦德雷格特，1992）。

2 小结

即使在计算机科学中，也有两个主要的研究分支类型系统，动态和静态的。

而更实用的，面向人工智能的，涉及到编程语言的应用，将是重点。