ATS is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages. 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. Wikipedia [ - ]

ATS is a programming language whose stated purpose is to support theorem proving in combination... [ + ]