Description #
ATS (Applied Type System) is a statically typed compiled language that blends functional and imperative paradigms, known for its ability to express advanced type systems — including dependent types — for high-assurance software.
History #
ATS was created by Hongwei Xi, a professor at Boston University, in the early 2000s. The language was designed to bridge the gap between formal methods and practical programming. ATS’s powerful type system allows programmers to encode invariants directly into types, enabling compile-time proofs of correctness.
Hello World Code #
implement main0 () = {
println! ("Hello, World!")
}How to Run #
Option 1: Online
https://play.ats-lang.org
Option 2: Local
- Install ATS2 from https://ats-lang.github.io
- Compile and run: bashCopyEdit
patscc hello.dats -o hello ./hello
Key Concepts #
- Syntax style: C-like with advanced type annotations
- Typing discipline: Strong, static, supports dependent and linear types
- Execution model: Compiled to C, then to native binary
- Common use cases: Systems programming, verifiable software, low-level safe programming
- Toolchain or ecosystem: ATS compiler (ATS2),
patscc, and libraries - Paradigms supported: Functional, imperative, concurrent
- Compilation details: ATS code is transpiled to C, then compiled with a C compiler
- Strengths or quirks: Proof-carrying code, zero-cost abstractions, fine-grained memory control
- Libraries/frameworks: Standard library plus external bindings to C
- Community/adoption: Niche academic and safety-critical software development circles
Try It Online #
Fun Facts #
ATS is one of the few practical programming languages that supports dependent types — allowing programs to encode proofs alongside logic. It’s often studied in formal methods and programming language theory courses.
