Welcome to Formality’s documentation!

Formality is an optimal functional programming language featuring theorem proving. It is similar to Agda and Idris in functionality, but takes a different approach to termination and induction: instead of a somewhat “hard-coded” structural recursion checker, it is based on Elementary Affine Logic, which gives it an elegant halting argument and complexity class, as well as great properties such as optimal substitutions, no garbage-collection, and an expressive type-theory with self-encoded inductive datatypes. To get a feel for how the language looks, please take a look at files such as Data.Bool.fm, Data.List.fm, Control.Functor.fm or Relation.Equality.fm from Formality-Base, our official standard libraries.