ATS：用定理证明编写可信代码
Introduction to Programming in ATS
这是一本关于 ATS 编程语言的入门指南，由 Hongwei Xi 撰写。书中不仅涵盖了基础函数式编程、递归数据类型和参数多态等核心概念，更深入探讨了依赖类型、线性类型以及定理证明在编程中的应用。ATS 允许开发者在编写代码的同时进行数学证明，确保程序逻辑的绝对正确性。虽然内容对初学者可能略显密集，但它为构建 Trustful Software 提供了强大的理论工具和实战路径，特别适合追求代码高可靠性的开发者。
作为一门编程语言，ATS 在语法和特性上都极其丰富。
- srean
ATS 以前在 HN 上讨论得挺多的
https://hn.algolia.com/?query=The%20ATS%20Programming%20Lang...
MLton 和 Felix 是另外两种受 ML 启发的语言，它们通过全程序优化来生成快速代码。
- ddellacosta
这里有个关于这门语言的有趣演讲：https://www.youtube.com/watch?v=zt0OQb1DBko（Aditya Siram 的《ATS 系统编程（不那么温和的）入门》）
- esafak
看起来很有趣。正在积极开发中：https://github.com/githwxi/ATS-Postiats
编辑：你说得对，我确实不知道还有第三个版本。要是这东西能有发布说明就好了。我完全不知道这门语言目前的状况如何。Hongwei，如果你在看的话！
如果这门语言想真正成气候，就需要社区来共同开发。