XKCD

http://xkcd.com/478/
What's that, Randall, still making jokes about your ex-girlfriend to conceal the fact that it matters to you?

What is ATS?

ATS is a programming language with a highly expressive type system rooted in the framework Applied Type System. In particular, both dependent types and linear types are available in ATS. The current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can be as efficient as C/C++ (see The Computer Language Benchmarks Game for concrete evidence) and supports a variety of programming paradigms that include:

Functional programming. While ATS is primarily a language based on eager call-by-value evaluation, it also supports lazy call-by-need evaluation. The availability of linear types in ATS can often make functional programs in ATS not only run with surprisingly high efficiency (when compared to C) but also run with surprisingly small (memory) footprint (when compared to C as well).

Imperative programming. The novel and unique approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem proving. While features considered dangerous in other languages (e.g., explicit pointer arithmetic and explicit memory allocation/deallocation) are allowed in ATS, the type system of ATS is still able to guarantee that no run-time errors can occur that may lead to memory corruption.

Concurrent programming. ATS, equipped with a multicore-safe implementation of garbage collection, can support multithreaded programming through the use of pthreads. There is also high-level support in ATS for parallel let-binding, which provides a simple and effective means to constructing programs that can take advantage of multicore architectures.

Modular programming. The module system of ATS is largely infuenced by that of Modula-3, which is both simple and general as well as effective in supporting large scale programming.

Expert programming. ATS has the most complicated type system is the universe, therefore it is very expert. The support for metalogical lambda calculus substructural coercsions and higher order metatheoretic properties is unrivaled.

In addition, ATS contains a component ATS/LF that supports a form of (interactive) theorem proving, where proofs are constructed as total functions. With this component, ATS advocates a programming style that combines programming with theorem proving. Furthermore, this component may be used as a logical framework to encode various deduction systems and their (meta-)properties.