Type theory was developed to be an alternative to set theory as the foundation of mathematical proofs in symbolic logic due to its ability to solve some contradictions stemming from naive set theory. — Where do Type Systems Come From?