How are programming languages and foundations of mathematics related?

[Note: this paragraphs is now outdated.] The title of your question contains an unwarranted assumption, namely that programming languages are “based on foundations of mathematics”. This is generally not the case, although the two areas do have important relationships. A more accurate statement would be that (some) programming languages were designed using foundational techniques. A better question to ask would be “how are programming languages and foundations of mathematics related?” The most general connection is embodied in the slogan proofs-as-programs, which can be made to work in several ways. The Curry-Howard correspondence is the most obvious one. With it we relate at once type theory, logic, and programming. But it should be emphasize that the Curry-Howard correspondence does not work very well in the presence of general recursion (because every type becomes inhabited), which every general-purpose programming language supports. A subtler way of making the slogan proofs-as-programs work is to use realizability. Here too we relate proofs and programs, but now the direction goes from proofs to programs: every proof gives a program, but not every program is necessarily a proof. The main example of a programming language based on a foundation is Agda, which simply is an implementation of dependent type theory. However, Agda is not a general-purpose programming language because it does not support general recursion. Every function in Agda is total, and there are computable functions which cannot be implemented in Agda. In practice programmers won’t notice this, but they will notice that Agda does not allow undefined values, for example infinite loops. Coq is not a programming language but rather a proof assistant. However, it too has extraction capabilities which give programs from proofs. Proof assistants and programming languages should not be confused with each other. We should not forget that prolog and other logic programming languages take their inspiration from the idea that computation is proof search. This of course relates them closely to logic. Haskell is a general-purpose programming language which is based on domain theory. That is to say, its semantics is domain-theoretic because it has to account for partial functions and recursion. The Haskell community has developed a number of techniques inspired by category theory, of which monads are best known but should not be confused with monads. More generally, advanced programming features are usually treated with a combination of domain theory and category theory, but this is not something that the Haskell programmer in the street is adept at. The so-called “syntactic category” of Haskell types is a lay man’s view of how Haskell and category theory correspond to each other. Set theory (classical or constructive) seems to inspire ideas in programming language to a lesser extent. Of course, constructive set theory has its connection to programming through constructive logic. One important application of intuitionistic set theory to programming languages was given by Alex Simpson who used it to make synthetic domain theory work. But this is quite advanced stuff, maybe see these slides. Jean-Louis Krivine has developed a very interesting brand of realizability for classical set theory. This seems a good way to relate classical set theory and programming. In summary, the theory of programming languages uses foundational techniques. This is not surprising, as we consider computation to be a fundamental concept. But it is too naive to say that programming languages are “based” on a certain foundations. In fact, the trichotomy of foundations “set theory — type theory — category theory” is again just a useful high-level observation that can be made mathematically precise in various ways, but there is nothing necessary about it. It is a historic accident.