ATS 编程语言

# ATS-PL-SYS 来源：https://www.cs.bu.edu/~hwxi/atslangweb/ --- ## 什么是 ATS？ ATS 是一种静态类型的编程语言，它将实现与形式化规约统一起来。该语言配备了一个高度表达力的类型系统，该系统根植于*应用类型系统*框架，这也是该语言名称的由来。特别地，ATS 中同时支持依赖类型和线性类型。 当前 ATS2（ATS/Postiats）的实现是用 ATS1（ATS/Anairiats）编写的，代码量超过 18 万行。ATS 在时间和内存效率上可与 C/C++ 媲美，并支持多种编程范式，包括： - **函数式编程**。ATS 的核心是一种受 ML 启发的按值调用的函数式语言。ATS 中线性类型的可用性常常使得用其编写的函数式程序不仅运行效率惊人（与 C 相比），而且内存占用也惊人地小（同样与 C 相比）。 - **命令式编程**。ATS 中命令式编程的新颖方法牢固地植根于*使用定理证明进行编程*的范式。ATS 的类型系统允许安全地支持许多在其他语言中被认为危险的功能（例如显式指针算术和显式内存分配/释放），这使得 ATS 非常适合实现高质量的低级系统。 - **并发编程**。ATS 可以通过安全使用 pthreads 来支持多线程编程。利用线性类型来跟踪和安全管理资源，为构建能够充分利用多核架构的可靠程序提供了一种有效方法。 - **模块化编程**。ATS 的模块系统很大程度上受到 Modula-3 的影响，它既简单又通用，并且能够有效地支持大规模编程。 此外，ATS 包含一个子系统 ATS/LF，它支持一种（交互式）定理证明形式，其中证明被构建为全函数。借助这个子系统，ATS 能够倡导一种*以程序员为中心*的程序验证方法，该方法以语法交织的方式将编程与定理证明结合起来。此外，ATS/LF 还可以作为一个逻辑框架（LF），用于对各种形式系统（如逻辑系统和类型系统）及其（元）性质证明进行编码。 --- ## ATS 适合做什么？ - ATS 可以极大地提高实际编程中的精确性。 - ATS 可以极大地促进基于细化的软件开发。 - ATS 允许程序员编写直接操作原生非装箱数据表示的高效函数式程序。 - ATS 允许程序员通过利用线性类型来减少程序的内存占用。 - ATS 允许程序员通过利用定理证明来增强程序的安全性（和效率）。 - ATS 允许程序员编写在操作系统内核中运行的安全低级代码。 - ATS 可以帮助教授类型理论，令人信服且具体地展示类型在构建高质量软件中的力量和潜力。 --- ## 学习 ATS 的建议 ATS 功能丰富（就像 C++ 一样）。事先具备基于 ML 的函数式编程和基于 C 的命令式编程知识，对学习 ATS 将有巨大帮助。一般来说，你将会在 ATS 中遇到许多不熟悉的编程概念和特性，并准备好花费大量时间学习它们。希望到最后，你将成为一个极其自信的程序员，能够享受构建大型复杂系统而几乎不需要调试的乐趣。 --- ## 致谢 ATS 的开发部分得到了美国国家科学基金会 (http://www.nsf.gov/) 的资助，资助编号为 CCR-0081316/CCR-0224244、CCR-0092703/0229480、CNS-0202067、CCF-0702665 和 CCF-1018601。一如既往，*本文所表达的任何观点、发现、结论或建议均为作者本人意见，并不一定反映 NSF 的观点。*