ATS is …

A statically typed programming language of precision and practicality. It unifies formal specification with implementation, enforcing effectively that a claimed implementation of a given specification must implement precisely according to the specification.

Read More …

ATS is good for …

* enforcing great precision in practical
  programming, and
* supporting functional programming with
  native data representation, and
* reducing memory footprint by employing
  linear types, and
* enhancing safety and efficiency through
  theorem-proving, and
* allowing direct interaction with C that
  incurs no run-time overhead, and
* generating high-quality code that runs
  in OS kernels, etc.

A Simple Example

Following is a complete program in ATS for printing out the string "Hello, world!" plus a newline:


implement main () = print ("Hello, world!\n")

Assume that the program is stored in a file named hello.dats. By executing the following command-line:
atscc -o hello hello.dats
we can generate an executable named hello, which does what is mentioned above if executed. The command atscc first compiles the ATS program contained in hello.dats into some C code and then invokes a C compiler (e.g., gcc) to translate the C code into binary object code.

Implementations

Acknowledgments

The development of ATS has been funded in part by National Science Foundation (NSF) under the grants no. CCR-0081316/CCR-0224244, no. CCR-0092703/0229480, no. CNS-0202067, no. CCF-0702665 and CCF-1018601. As always, any opinions, findings, and conclusions or recommendations expressed here are those of the author(s) and do not necessarily reflect the views of the NSF.