Athena is a programming language and environment for proof engineering and natural deduction.
As a programming language, Athena is an expressive, higher-order functional language inspired by ML and Scheme.
Modern software engineers often work with large codebases & even larger sets of dependencies. Modern languages and developer tools are successful to the extent that they help developers manage the complexity of their projects. Athena provides many of the utilities and conveniences to the proof engineering process that those in the software engineering industry have grown to expect from modern technology. To this end, Athena provides:
- A flexible module system for organizing large scale projects.
- Structured theories as data types, affording the construction of theory hierarchies related by abstraction and refinement for maximum reusability.
- Higher order deductions, which enable the development of higher level, custom proof procedures much the same way one would define reusable functions or classes in software development.
- The ability to “stub” all or parts of a given proof, making it easy to incrementally check one’s work, just as a software developer would via special macros (like Rust’s
todo!()) and mocked function calls. - An accessible syntax designed to be as similar as possible to “proofs on paper” in natural deduction.
Athena has numerous powerful features & benefits, including:
- Equational reasoning and term rewriting, providing the capabilities for writing formal executable specifications.
- Built-in integration with industry-grade automated theorem provers (ATPs) and SMT solvers.
- Many-sorted first order logic with Hindley-Milner style polymorphism.
- First class functions and proof tactics.
- Support for mathematical, structural and strong induction.
- Pattern matching