Modern Type Theory (usually called Homotopy Type Theory) is at the
same time the ultimate functional programming language and a novel
foundation of Mathematics, an alternative to the mathematical assembly
language called set theory. Type theory exploits the advantages of
static typing to the limit, meaning that by hiding implementation
details you can identify tow object which behave the same - this is
called the univalence principle.