This repo contains a specification for a language designed to run on a virtual machine constructed from mathematics. The language aims to be simple enough for any programmer to immediately use, but powerful enough to provide fast proofs of large programs.