ATS：使用定理证明进行编程/前言

本书旨在使用 ATS 教授实用的编程技能：我们专注于实际编写程序，本书不涵盖编程的其他方面，例如制定问题描述、思考问题以及使用各种解决问题技巧。ATS 与其他编程语言（即 Standard ML 和 OCaml）共享某些方面，但在使用其类型系统支持安全（就类型安全性而言）和高效（就执行时间和内存占用而言）的多种范式编程方面非同寻常。

ATS 支持命令式、函数式和并发编程范式。命令式编程是大多数程序员熟悉的。函数式编程可以与命令式编程形成对比，因为它使程序员能够专注于手头的任务，而不必过多担心（无关紧要的）某种实现细节，例如显式内存管理。一些函数式程序可以被视为可执行的规范，这使得它们适合于教学和推理。

众所周知，编程容易出错（“错误”是指“不希望的程序行为”）。缓解问题的一种方法是进行广泛的测试，但有时，您会想要使用其他方法，例如在类型系统的帮助下，正式声明前置条件、后置条件和其他不变式。

类型系统已成为一种工具，用于消除某些类别的程序错误（例如，确保为对象分配内存并正确初始化）。

典型的类型安全编程语言（例如 Pascal 和 Java）不会尝试将整数类型的变量视为布尔类型的变量；这类错误在编译时（早期，在测试之前）被排除。其他错误，例如数组越界访问，无法在编译时检查，因此这些检查将移至下一阶段，即执行程序。该程序保持安全（从某种意义上说），因为即使它出错，它也不会继续出错。

此外，公共 API 通常会在其使用中设置某些限制以使其正常运行。例如，如果将 NULL 传递给格式字符串，[printf] 会做什么？在典型的静态类型编程语言中，不可能强制执行对 [printf] 的编译时约束：它只接受非 NULL 格式字符串。此外，还有一些规则必须在构建格式字符串时遵循。

这就是 ATS 的用武之地：它允许您，程序员，使用其类型系统正式指定约束。然后，编译器会在没有人为干预的情况下检查这些约束。例如，在 ATS 中，您可以选择（权衡）证明您的程序永远不会越界访问数组，从而使运行时边界检查变得多余，并增加我们的信心。在这种特定情况下，您无需通过测试来解决此问题。

我们强烈建议我们的读者不要考虑他们对常见静态类型编程语言（尤其是 C/C++）的经验，因为这种经验在很大程度上不适用于使用 ATS 进行编程（因为您不会在这些语言中使用类型来表达约束）；并保持开放的心态，接受新的想法和概念，这些想法和概念起初可能看起来令人困惑，但我们希望在练习一段时间后就能理解。

第一章介绍了 ATS 的纯函数式子集，从基本算术开始，一直到函数和数据结构。在本章中，读者将熟悉没有赋值和循环的编程。第二章介绍了基本的命令式编程（可变变量和数据结构、显式控制流运算符），并将其与第一章介绍的语言相关联。第三章将介绍类型方面的知识，然后介绍一些高级类型，例如单例类型、依赖类型和线性类型。第四章向用户介绍了使用类型进行程序验证。