ATS: Programming with Theorem-Proving/Preface

This book is aimed at teaching practical programming skills using ATS: we concentrate on actually writing programs, all other aspects of programming, such as formulating problem descriptions, thinking about them, and using various problem solving techniques are not covered in this book. ATS shares some aspects with other programming languages, namely Standard ML and OCaml, but is unusual in the way it uses its type system to support safe (in terms of type safety) and efficient (in terms of execution time and memory footprint) programming in a variety of paradigms.

ATS supports imperative, functional and concurrent programming paradigms. Imperative programming is what most programmers are familiar with. Functional programming can be contrasted with imperative programming as it enables programmers to concentrate on the problem at hand without worrying too much about (uninteresting) implementation details of some kind, such as explicit memory management. Some functional programs can be seen as executable specifications, which makes them suitable for teaching and reasoning about.

It is widely known that programming is prone to errors (by "error" we mean "unwanted program behavior"). One way to mitigate the problem is extensive testing, but sometimes, you'll want to use other methods, such as stating pre-, post-conditions and other invariants formally, with help of a type system.

Type systems have arisen as a tool to eliminate certain classes of program errors (for example, making sure that memory for an object is allocated and initialized correctly).

Typical type-safe programming languages (such as Pascal and Java) will not try to treat a variable of type integer as if it was a variable of type bool; errors like this are ruled out at compile-time (early, before testing). Other errors, such as out-of-bounds array access, cannot be checked at compile-time, hence such checks are moved on to the next phase, of executing the program. The program remains safe (in a sense), because even if it goes wrong, it will not continue to do so.

Also, it's usually the case that public APIs place certain restrictions on their use for proper functioning. For example, what would [printf] do if the NULL was passed for the format string? In a typical statically typed programming language it is not possible to enforce a compile-time constraint on [printf]: it accepts only non-NULL format strings. In addition, there are rules that must be followed in constructing format strings.

This is where ATS fits in: it allows you, the programmer, to formally specify constraints using its type system. Such constraints are then checked by the compiler without human intervention. For example, in ATS you have an option (a trade-off) to prove that your program will never access an array out of its bounds making run-time bounds-checking redundant and increasing our confidence. In this particular case, you won't need to address this issue with tests.

We heartily recommend our readers to not take into account their experience with common statically typed programming languages (especially C/C++) because this experience, for the most part, is not applicable to programming with ATS (as you don't use types in these languages to express constraints); and to keep their mind open for new ideas and concepts, which might seem confusing at first, but we hope will make sense after some practice.

Chapter one contains an introduction to a purely functional subset of ATS, starting from elementary arithmetic, continuing to functions and data structures. In this chapter, readers will acquaint themselves with programming without assignment and loops. Chapter two covers basic imperative programming (mutable variables and data structures, explicit control flow operators) and relates it to the language introduced in chapter one. Chapter three goes to a detour about types, and then introduces some advanced types, such as singleton types, dependent and linear types. Chapter four introduces users to program verification with types.