ATS：使用定理證明進行程式設計
ATS 是一種將規範和實現統一的程式語言。它配備了高度表達的型別系統，其根源在於應用型別系統框架，這也是該語言名稱的來源。在 ATS 中，支援多種程式設計正規化，包括函數語言程式設計、指令式程式設計、（有限形式的）面向物件程式設計、模組化程式設計等。此外，ATS 包含一個定理證明元件 ATS/LF，允許將證明構建為完整函式。藉助此元件，ATS 提倡以程式設計師為中心的程式驗證方法，將程式設計與定理證明相結合：我們如何知道程式是否正確實現？我們要求實現程式的程式設計師也構建一個證明，證明該程式滿足其規範。此外，定理證明元件 ATS/LF 可用作邏輯框架，用於對各種演繹系統及其（元）屬性進行編碼。
ATS 的獨特之處在於它強調使用型別和證明來確保程式安全。例如，在 ATS 中可以靜態地（即在編譯時）排除空指標取消引用；可以靜態地排除陣列下標越界；可以靜態地排除記憶體的錯誤處理，如記憶體洩漏和雙重釋放等。更重要的是，ATS 為程式設計師提供了極大的靈活性，讓他們可以設計一種基於型別的方法來捕獲他們感興趣的特定安全違規行為。
本華夏公益教科書旨在向您介紹 ATS 程式語言，從基礎知識到最先進的功能，它旨在成為官方教程的替代性演示。我們並不旨在教授您程式設計，為此您應該參考其他書籍（例如 HtDP）。