Formality é uma linguagem de programação funcional em desenvolvimento, e que será lançada oficialmente ainda esse ano. Ela é uma linguagem bem "hardcore", com tipos dependentes e provas formais, inspirada em Haskell/Agda/Coq, mas com uma série de diferenciais, principalmente no que diz respeito ao runtime (optimal reductions, paralelismo, runtime fusion, etc.), visando combinar todo esse alto nível matemático com o potencial de ser realmente eficiente na prática. Essa é a carinha atual dela:
// Datatypes estilo Haskell
// O tipo de números naturais
T Nat
| succ {pred : Nat}