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.
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.datswe 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.