Building ATS2 from Source in 2026

Summary

I wanted to look at ATS again after a long gap. I've written about it many times before but haven't done much with it in recent years. Part of what prompted this was looking at Verus for verified Rust programming and thinking about how ATS compares. ATS takes a different approach to verification. It's built into the type system itself rather than added as an annotation layer. Proofs are first-class values that you construct and pass around. It compiles to C and the proofs are erased during compilation so the generated code is just plain C with no runtime overhead. In this post I go through the steps I needed to build ATS1 and ATS2 from their GitHub repositories on Linux and macOS. I expected this to be straightforward but ended up spending a fair amount of time working through bitrot in the existing documentation and build system. # Bitrot The last official ATS2 release was version 0.4.2 in 2020. Development has continued on GitHub but there hasn't been a new release tarball. The ATS website still links to older releases. Most of the build instructions I found online are out of date or refer to release tarballs that aren't the best way to get started anymore. Building from the GitHub repositories requires building ATS1 (ATS-Anairiats) first since the ATS2 compiler is written in ATS1. This is where most of the problems are. The ATS1 repository has broken autotools symlinks, missing directories and issues with newer versions of macOS. I spent some time working through these and documenting the fixes here. # Prerequisites On Linux (Debian/Ubuntu) the dependencies are straightforward: $ sudo apt-get install -y build-essential automake bison libgmp-dev On macOS with Homebrew there are a few extra steps. Install the dependencies: $ brew install automake bison gmp gcc Homebrew's bison needs to be added to the PATH because macOS ships an older version that is too old for the ATS1 build: $ export PATH="/opt/homebrew/opt/bison/bin:$PATH" This is for Apple Silicon. On Intel Ma...