Formality exists to fill a hole in the current market: there aren’t many languages featuring theorem proving that are simple, user-friendly and efficient. To accomplish that goal, we rely on several design philosophies:
An accessible syntax¶
Fast and portable “by design”¶
An optimal high-order evaluator¶
An elegant underlying Type Theory¶
Formality’s unique approach to termination is conjectured to allow it to have elegant, powerful type-level features that would be otherwise impossible without causing logical inconsistencies. For example, instead of built-in datatypes, we rely on Self Types, which allow us to implement inductive families with native lambdas. As history tells, having elegant foundations often pays back. We’ve not only managed to port several proofs from other assistants, but found techniques to emulate Coq’s structural recursion, to perform large eliminations, and even an hypothetical encoding of higher inductive types; and we’ve barely began exploring the system.
Interaction Net (inet) simulation