ATS：使用定理证明进行编程
ATS 是一种将规范和实现统一的编程语言。它配备了高度表达的类型系统，其根源在于应用类型系统框架，这也是该语言名称的来源。在 ATS 中，支持多种编程范式，包括函数式编程、命令式编程、（有限形式的）面向对象编程、模块化编程等。此外，ATS 包含一个定理证明组件 ATS/LF，允许将证明构建为完整函数。借助此组件，ATS 提倡以程序员为中心的程序验证方法，将编程与定理证明相结合：我们如何知道程序是否正确实现？我们要求实现程序的程序员也构建一个证明，证明该程序满足其规范。此外，定理证明组件 ATS/LF 可用作逻辑框架，用于对各种演绎系统及其（元）属性进行编码。
ATS 的独特之处在于它强调使用类型和证明来确保程序安全。例如，在 ATS 中可以静态地（即在编译时）排除空指针取消引用；可以静态地排除数组下标越界；可以静态地排除内存的错误处理，如内存泄漏和双重释放等。更重要的是，ATS 为程序员提供了极大的灵活性，让他们可以设计一种基于类型的方法来捕获他们感兴趣的特定安全违规行为。
本维基教科书旨在向您介绍 ATS 编程语言，从基础知识到最先进的功能，它旨在成为官方教程的替代性演示。我们并不旨在教授您编程，为此您应该参考其他书籍（例如 HtDP）。