ATS (programming language)

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages) This article relies excessively on references to primary sources. Please improve this article by adding secondary or tertiary sources. Find sources: "ATS" programming language – news · newspapers · books · scholar · JSTOR (March 2018) (Learn how and when to remove this message) This article is written like a manual or guide. Please help rewrite this article and remove advice or instruction. (February 2020) This article may be too technical for most readers to understand. Please help improve it to make it understandable to non-experts, without removing the technical details. (September 2020) (Learn how and when to remove this message) (Learn how and when to remove this message)

ATS

Paradigms	multi-paradigm: functional, imperative, object-oriented, concurrent, modular
Family	ML: Caml: OCaml: Dependent ML
Designed by	Hongwei Xi
Developer	Boston University
First appeared	2006; 18 years ago (2006)
Stable release	ATS2-0.4.2[1] / November 14, 2020; 3 years ago (2020-11-14)
Typing discipline	static, dependent
License	GPLv3
Filename extensions	.sats, .dats, .hats
Website	www.ats-lang.org
Influenced by
Dependent ML, ML, OCaml, C++

In computing, ATS (Applied Type System) is a multi-paradigm, general-purpose, high-level, functional programming language. It is a dialect of the programming language ML, designed by Hongwei Xi to unify computer programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems.^[2] A past version of The Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the languages C and C++.^[3] By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such as division by zero, memory leaks, buffer overflow, and other forms of memory corruption by verifying pointer arithmetic and reference counting before the program compiles. Also, by using the integrated theorem-proving system of ATS (ATS/LF), the programmer may make use of static constructs that are intertwined with the operative code to prove that a function conforms to its specification.

ATS consists of a static component and a dynamic component. The static component is used for handling types, whereas the dynamic component is used for programs. While ATS primarily relies on a call-by-value functional language at its core, it possesses the ability to accommodate diverse programming paradigms, such as functional, imperative, object-oriented, concurrent, and modular.