A dependently typed, imperative, bare-metal programming language.