An efficient proof-gramming language. It aims to be:
Fast: no garbage-collection, optimal beta-reduction and a massively parallel GPU compiler make it fast.
Safe: a type system capable of proving mathematical theorems about its own programs make it secure.
Portable: the full language is implemented in a 400-LOC runtime, making it easily available everywhere.
safe_head(A; xs: List(A), e: length(_ xs) != 0n) : A case xs + e : length(_ xs) != 0n | nil => absurd(e(refl(__)), _) -- provably unreachable! | cons => xs.head