How are programming languages and foundations of mathematics related?

Question

Basically I am aware of three foundations for math

1. Set theory
2. Type theory
3. Category theory

So in what ways are programming languages and foundations of mathematics related?

EDIT

The original question was "Programming languages based on foundations of math"

with the added paragarph of

And implementations of theory
1. Type theory in Coq
2. Set theory in SETL
3. Category theory in Haskell

Based on a suggestion this was changed to "How are programming languages and foundations of mathematics related"

Since this is one of those questions were I did not know enough about what I was asking but wanted to learn something, I am modifing the question to make it more valuable for learning and others, yet leaving the details in so as not to make the current answer by Andrej Bauer seem off topic.

Thanks for all the comments and the answer so far, I am learning from them.

Answer 1

[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.

Answer 2

this is a very complex topic and there are many great books on the subject, a recent one is called Turings Cathedral, origins of the digital universe and also Engines of logic, mathematicians and the origins of the computer.

computer languages have evolved over many decades, but believe it or not there are two original programming languages which show that mathematics and computer science are intimately intertwined:

• Turing's 1936 paper on the halting problem. a theoretical construction to solve the problem proposed by hilbert at the turn of the century, the Entscheidungsproblem, ie an automated procedure to solve mathematical problems!

• Church's lambda calculus developed at the same time still survives in languages like lisp and scheme

there are two key figures who crossed mathematical and computer science boundaries wrt "programming languages":

• information theory pioneered by Shannon shows the deep connections between mathematics and computer science

• another key figure that crosses between mathematics and computer science is Von Neumann. he invented the von neumann architecture of storing programs in memory.

even earlier "programming languages":

• the english word "computer" originally meant something more like a "calculator" that used mathematical operations on numbers and its meaning has shifted substantially to the general-purpose programming concept of today. so there is a connection between programming languages and early calculators.
• punch cards used in weaving looms from the late 19th and early 20th century were a "programming language" for weaving patterns. note that punch cards were used for programming mainframes much in the 1960s. these were originally seen as "calculating machines" (using mathematics!) not so much modern, general purpose computers.
• Babbage and Ada Lovelace developed the rudimentary early concepts of "programming languages" in the mid 1800s on a "calculating engine"
• boolean algebra was originally a purely mathematical concept invented by Boole
• the ancient (millenia old) abacus for mathematical calculation is seen as a forerunner of the modern computer. but it could be said that operations for manipulating it were a sort of "programming language" (followed by humans)

however, in modern programming languages as the abstraction has increased and scaled, the clear, direct connection to mathematics has somewhat decreased over the decades, but its always going to be quite intrinsic and in some ways, it has strengthened. for example languages such as Java with its strict types has connections to mathematics, and in the starting in the late ~1990s mainstream computer languages (eg c++, Java, Ruby etc) started explicitly implementing many mathematical higher-level objects as near primitives in the languages such as sets, trees (eg Btrees or hashmaps), etc.