3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic

3. I am not sure what GP meant with this, but I do know that in type theory, intuitionistic logic is very important. The propositions of intuitionistic logic correspond exactly to the types of types programs in certain models of programming languages, and the proofs of intuitionistic logic to well-typed programs in those models. This is called the Curry-Howard isomorphism, and has been a very fruitful source of inspiration for type theory. For example, it was originally noted for intuitionistic propositional logic only, but adding universal quantification gives a type theory with so-called parametric polymorphism, which was later developed into generics in Java and other languages. I have seen modal logic used to model distributed computation, and linear logic inspired work which eventually led to Rust's borrow checker.