In computing, ATS is a programming language designed by Hongwei Xi to unify programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems. Wikipedia