Como estão relacionadas as linguagens de programação e os fundamentos da matemática?

Basicamente, eu estou ciente de três fundamentos para a matemática

1. Teoria de conjuntos
2. Teoria dos tipos
3. Teoria das categorias

Então, de que maneiras as linguagens de programação e os fundamentos da matemática estão relacionados?

EDITAR

A pergunta original era "Linguagens de programação baseadas em fundamentos da matemática"

com o paragarfo adicionado de

E implementações da teoria
1. Teoria dos tipos em Coq
2. Teoria dos conjuntos em SETL
3. Teoria das categorias em Haskell

Com base em uma sugestão, isso foi alterado para "Como as linguagens de programação e os fundamentos da matemática estão relacionados"

Como essa é uma daquelas perguntas em que eu não sabia o suficiente sobre o que estava perguntando, mas queria aprender alguma coisa, estou modificando a pergunta para torná-la mais valiosa para a aprendizagem e outras, deixando os detalhes para não A resposta atual de Andrej Bauer parece fora de tópico.

Obrigado por todos os comentários e respostas até agora, estou aprendendo com eles.

[Nota: esses parágrafos agora estão desatualizados.] O título da sua pergunta contém uma suposição injustificada, ou seja, que as linguagens de programação são "baseadas em fundamentos da matemática". Geralmente, esse não é o caso, embora as duas áreas tenham relacionamentos importantes. Uma declaração mais precisa seria que (algumas) linguagens de programação foram projetadas usando técnicas fundamentais. Uma pergunta melhor a ser feita seria "como as linguagens de programação e os fundamentos da matemática estão relacionados?"

A conexão mais geral é incorporada no slogan provas como programas , que pode ser feito para funcionar de várias maneiras. A correspondência de Curry-Howard é a mais óbvia. Com ele, relacionamos de uma só vez teoria, lógica e programação de tipos. Mas deve-se enfatizar que a correspondência de Curry-Howard não funciona muito bem na presença de recursão geral (porque todo tipo se torna habitado), suportado por toda linguagem de programação de uso geral.

Uma maneira mais sutil de fazer funcionar o slogan de provas como programas é usar a realização . Também aqui relacionamos provas e programas, mas agora a direção vai de provas para programas: toda prova fornece um programa, mas nem todo programa é necessariamente uma prova.

O principal exemplo de uma linguagem de programação baseada em uma fundação é o Agda , que simplesmente é uma implementação da teoria dos tipos dependentes. No entanto, o Agda não é uma linguagem de programação de uso geral porque não suporta recursão geral. Todas as funções do Agda são totais e existem funções computáveis ​​que não podem ser implementadas no Agda. Na prática, os programadores não perceberão isso, mas perceberão que a Agda não permite valores indefinidos, por exemplo, loops infinitos.

Coq não é uma linguagem de programação, mas um assistente de prova. No entanto, também possui recursos de extração que fornecem programas de provas. Assistentes de prova e linguagens de programação não devem ser confundidos.

Não devemos esquecer que o prólogo e outras linguagens de programação lógica se inspiram na idéia de que a computação é uma prova de pesquisa . É claro que isso os relaciona de perto com a lógica.

Haskell é uma linguagem de programação de uso geral baseada na teoria de domínio . Ou seja, sua semântica é teórica do domínio, porque deve levar em conta funções parciais e recursão. A comunidade Haskell desenvolveu várias técnicas inspiradas na teoria das categorias, das quais as mônadas são mais conhecidas, mas não devem ser confundidas com as mônadas . De maneira mais geral, os recursos avançados de programação geralmente são tratados com uma combinação de teoria de domínio e teoria de categoria, mas isso não é algo que o programador Haskell na rua é adepto. A chamada "categoria sintática" dos tipos de Haskell é a visão de um leigo de como Haskell e a teoria da categoria se correspondem.

A teoria dos conjuntos (clássica ou construtiva) parece inspirar idéias em linguagem de programação em menor grau. Obviamente, a teoria dos conjuntos construtivos tem sua conexão com a programação por meio da lógica construtiva. Uma aplicação importante da teoria dos conjuntos intuicionista às linguagens de programação foi dada por Alex Simpson, que a usou para fazer a teoria do domínio sintético funcionar. Mas isso é algo bastante avançado, talvez veja esses slides . Jean-Louis Krivine desenvolveu uma marca muito interessante de realizabilidade para a teoria clássica dos conjuntos. Essa parece uma boa maneira de relacionar a teoria dos conjuntos clássica e a programação.

Em resumo, a teoria das linguagens de programação utiliza técnicas fundamentais. Isso não é surpreendente, pois consideramos a computação um conceito fundamental. Mas é ingênuo dizer que as linguagens de programação são "baseadas" em certas bases. De fato, a tricotomia das fundações "teoria dos conjuntos - teoria dos tipos - teoria das categorias" é novamente apenas uma observação de alto nível útil que pode ser matematicamente precisa de várias maneiras, mas não há nada necessário. É um acidente histórico.

este é um tópico muito complexo e há muitos livros excelentes sobre o assunto, um recente é chamado Catedral de Turings, origens do universo digital e também Motores de lógica, matemáticos e origens do computador .

as linguagens de computador evoluíram ao longo de muitas décadas, mas acredite ou não, existem duas linguagens de programação originais que mostram que a matemática e a ciência da computação estão intimamente entrelaçadas:

• O artigo de Turing de 1936 sobre o problema da parada . uma construção teórica para resolver o problema proposto por hilbert na virada do século, o Entscheidungsproblem , ou seja, um procedimento automatizado para resolver problemas matemáticos!

• O cálculo lambda da Igreja, desenvolvido ao mesmo tempo, ainda sobrevive em idiomas como lisp e schema

existem duas figuras-chave que cruzaram os limites matemáticos e da ciência da computação em "linguagens de programação":

• A teoria da informação, pioneira em Shannon, mostra as profundas conexões entre matemática e ciência da computação

• outra figura-chave que cruza a matemática e a ciência da computação é Von Neumann . ele inventou a arquitetura von neumann de armazenar programas na memória.

ainda mais "linguagens de programação":

• a palavra em inglês "computador" originalmente significava algo mais como uma "calculadora" que usava operações matemáticas em números e seu significado mudou substancialmente para o conceito de programação de uso geral de hoje. portanto, há uma conexão entre linguagens de programação e calculadoras iniciais.
• os cartões perfurados usados ​​nos teares do final do século XIX e início do século XX eram uma "linguagem de programação" para os padrões de tecelagem. note que cartões perfurados foram usados ​​para programar mainframes nos anos 60. estes eram originalmente vistos como "máquinas de calcular" (usando a matemática!), não como computadores modernos e de uso geral.
• Babbage e Ada Lovelace desenvolveram os primeiros conceitos rudimentares de "linguagens de programação" em meados do século XIX em um "mecanismo de cálculo"
• álgebra booleana era originalmente um conceito puramente matemático inventado por Boole
• o antigo ábaco (milênios) para cálculo matemático é visto como o precursor do computador moderno. mas pode-se dizer que as operações para manipulá-lo eram uma espécie de "linguagem de programação" (seguida por humanos)

no entanto, nas linguagens de programação modernas, à medida que a abstração aumenta e aumenta, a conexão clara e direta com a matemática diminuiu um pouco ao longo das décadas, mas sempre será bastante intrínseca e, de certa forma, foi fortalecida. por exemplo, linguagens como Java, com seus tipos estritos, tem conexões com a matemática e, no início dos anos 90, as principais linguagens de computador (por exemplo, c ++, Java, Ruby etc.) começaram a implementar explicitamente muitos objetos matemáticos de nível superior, como primitivos no idiomas como conjuntos, árvores (por exemplo, Btrees ou hashmaps), etc.