Type theory: a bridge between mathematics and computer science through
a set theory where sets are types and proofs are programs.