这是 Hongwei Xi 所著《Introduction to Programming in ATS》的在线版。书按层次介绍 ATS 的核心特性：函数式编程基础、简单类型、（递归定义的）数据类型、多态类型、依赖类型、线性类型、定理证明，以及「带定理证明的编程」（PwTP）与模板式编程。序言给出动机：软件规范常停留在口头讨论、纸笔草图或 UML 建模，而实现一旦与规范分道扬镳，规范就逐渐失去参考价值，实现本身变成新的规范，维护者越来越难改，用户越来越难学。ATS 受 Martin-Löf 的构造类型论启发，把规范与实现合进一门语言：静态部分（statics）管类型、动态部分（dynamics）管程序，规范写在 statics 里，再由定理证明子系统验证实现是否真的满足规范。作者说，如果只能给 ATS 一个词，那会是「精确」。