ATS: Programming with Theorem-Proving
ATS is a programming language that unifies specification and implementation. It is equipped with a highly expressive type system rooted in the framework Applied Type System, which also gives the language its name. In ATS, a variety of programming paradigms are supported, including functional programming, imperative programming, (a restricted form of) object-oriented programming, modular programming, etc. In addition, ATS contains a theorem-proving component ATS/LF that allows proofs to be constructed as total functions. With this component, ATS advocates a programmer-centric approach to program verification that combines programming with theorem proving: How do we know that a program is correctly implemented? We ask the programmer implementing the program to also construct a proof attesting to that the program meets its specification. Furthermore, the theorem-proving component ATS/LF may be used as a logical framework for encoding various deduction systems and their (meta-)properties.
What makes ATS distinctive is its emphasis on employing types and proofs to ensure program safety. For example, dereferencing null-pointers can be ruled out in ATS statically, i.e., at compile-time; out-of-bounds array subscripting can be ruled out statically; improper handling of memory such as leaking and double-freeing can be ruled out statically; etc. More importantly, ATS offers the programmer a great deal of flexibility in designing a type-based approach to capturing specific safety violations that he or she is interested in.
This wikibook is aimed to introduce you to the ATS programming language, from the basics to the most advanced features and is positioned be an alternative presentation of the official tutorial. We do not aim to teach you programming, for which you should consult other books (e.g. HtDP).