Athena is a programming language and an interactive theorem proving environment rolled in one. As a programming language, Athena is a higher-order functional language in the tradition of Scheme and ML: strict and lexically scoped. It encourages a programming style based on function calls and recursion, but it also offers imperative features (e.g. ML-style updateable memory cells) that can be used as an escape hatch for the sake of efficiency. As a theorem proving system, Athena is based on many-sorted first-order logic. Many-sorted first-order logic is a very expressive language; some logicians (e.g. Maria Manzano in her ”Extensions of first-order logic”) have argued that it can be viewed as a unifying framework for all other logics, including higher-order logic. It retains the tractability of first-order logic (completeness, compactness, structural induction over terms and formulas, efficient matching and unification algorithms, etc.), while overcoming some of the modeling awkwardness of single-sorted logic. Athena adds Hindley-Milner-style polymorphism to many-sorted logic, which further increases its flexibility.