ATS-LANG-ORG

ats-lang.github.io

For hosting certain parts of ats-lang.org

Resources

What is ATS?

Let me first paraphrase Prof. John Reynolds. A programming language should be simple and general; it should possess a (highly) efficient implementation and allow for (highly) extensive error-checking both statically and dynamically. And I now add my own. A programming language should also (greatly) enhance programming productivity through its forever expanding meta-programming support. ATS aspires to be such a superman programing language, and it is becoming one.

ATS is a statically typed programming language originally designed to unify implementation with formal specification. It is equipped with a highly expressive type system rooted in the framework Applied Type System, which gives the language its name. In particular, both dependent types and linear types are available in ATS.

What is ATS good for?

ATS can greatly enforce precision in practical programming.
ATS can greatly facilitate refinement-based software development.
ATS allows the programmer to write efficient functional programs that directly manipulate native unboxed data representation.
ATS allows the programmer to reduce the memory footprint of a program by making use of linear types.
ATS allows the programmer to enhance the safety (and efficiency) of a program by making use of theorem-proving.
ATS allows the programmer to write safe low-level code that runs in OS kernels.
ATS can help teach type theory, demonstrating both convincingly and concretely the power and potential of types in constructing high-quality software.

Suggestion on learning ATS

ATS is feature-rich (like C++). Prior knowledge of functional programming based on ML and imperative programming based on C can be a big plus for learning ATS. In general, one should expect to encounter many unfamiliar programming concepts and features in ATS and be prepared to spend a substantial amount of time on learning them. Hopefully, one will become a superbly confident programmer at the end who can enjoy implementing large and complex systems with minimal need for debugging.