In 2017 the Russian mathematician and Fields Medalist Vladimir Voevodsky died at age 51. Voevodsky once discovered a severe error in one of his papers that was already published for years which motivated him to learn using the computer proof assistant Coq. A proof assistant is a program which can verify mathematical proofs and also provides assistance in the process of writing the proofs (such as showing which parts are still open). The basis of Coq and of many other proof assistants isn't set theory as one might expect, but type theory (or more specifically: the calculus of inductive constructions, a version of typed lambda calculus), a theory in which the basic objects are not sets but functions with specific "types" of domains and codomains. A typical type theoretic statement might be: If f is a function from A to B ("of type A -> B") and g is a function from B to C, then the composition of g and f is a function from A to C. This may sound trivial but it turns out that a sufficiently rich axiomatic description of the behavior of pure functions (which is typed lambda calculus) can serve as an alternative to set theory as a basis of mathematics that has one decisive advantage: A "proof" of some statement (theorem) is not a meta-object of the theory (as it is in set theory where a "proof" is not a set itself but a sort of "tree" of set theoretic statements) but is itself an object of the theory: in type theory a proposition (theorem) is a type and a proof is a function of that type. The type A -> B of functions from A to B is interpreted as the statement "A implies B" and a function "f:A -> B" that has this type is interpreted as a proof of that statement (it is a function which maps proofs of statement A to proofs of statement B which is exactly what implication means). This is the so-called Curry-Howard isomorphism or PAT interpretation of typed lambda calculus, where PAT stands for both "Propositions As Types" and "Proofs As Terms".