[Uwaga: akapity te są obecnie nieaktualne.] Tytuł twojego pytania zawiera nieuzasadnione założenie, że języki programowania są „oparte na podstawach matematyki”. Zasadniczo tak nie jest, chociaż te dwa obszary mają ważne relacje. Bardziej dokładnym stwierdzeniem byłoby, że (niektóre) języki programowania zostały zaprojektowane przy użyciu podstawowych technik. Lepszym pytaniem byłoby „w jaki sposób powiązane są języki programowania i podstawy matematyki?”
Najbardziej ogólne połączenie zawarte jest w sloganie proof-as-program , który może działać na kilka sposobów. Korespondencja Curry-Howard jest najbardziej oczywista. Dzięki niemu od razu łączymy teorię, logikę i programowanie typów. Należy jednak podkreślić, że korespondencja Curry-Howarda nie działa zbyt dobrze w przypadku ogólnej rekurencji (ponieważ każdy typ staje się zamieszkały), którą obsługuje każdy język programowania ogólnego przeznaczenia.
Subtelniejszym sposobem sprawienia, by hasło działało jako proof-as-programy, jest wykorzystanie wykonalności . Tutaj również odnosimy proofy i programy, ale teraz kierunek przechodzi od proofów do programów: każdy dowód daje program, ale nie każdy program jest koniecznie dowodem.
Głównym przykładem języka programowania opartego na fundamencie jest Agda , która jest po prostu implementacją teorii typów zależnych. Jednak Agda nie jest językiem programowania ogólnego, ponieważ nie obsługuje ogólnej rekursji. Każda funkcja w Agdzie jest sumą i istnieją funkcje obliczalne, których nie można zaimplementować w Agdzie. W praktyce programiści tego nie zauważą, ale zauważą, że Agda nie dopuszcza niezdefiniowanych wartości, na przykład nieskończonych pętli.
Coq to nie język programowania, ale raczej dowodem asystent. Ma jednak również możliwości ekstrakcji, które dają programy z dowodów. Proof asystentów i języków programowania nie należy mylić ze sobą.
Nie powinniśmy zapominać, że prolog i inne logiczne języki programowania czerpią inspirację z idei, że obliczenia są wyszukiwaniem dowodów . To oczywiście wiąże je ściśle z logiką.
Haskell to uniwersalny język programowania oparty na teorii domen . Innymi słowy, jego semantyka ma charakter teoretyczny, ponieważ musi uwzględniać funkcje cząstkowe i rekurencję. Społeczność Haskell opracowała szereg technik inspirowanych teorią kategorii, z których najlepiej znane są monady, ale nie należy ich mylić z monadami . Mówiąc bardziej ogólnie, zaawansowane funkcje programowania są zwykle traktowane za pomocą kombinacji teorii domen i teorii kategorii, ale nie jest to coś, do czego biegły jest programista Haskell na ulicy. Tak zwana „kategoria syntaktyczna” typów Haskella jest świeckim poglądem na to, w jaki sposób Haskell i teoria kategorii odpowiadają sobie nawzajem.
Teoria zbiorów (klasyczna lub konstruktywna) wydaje się inspirować pomysły w języku programowania w mniejszym stopniu. Oczywiście teoria mnogości konstruktywnych ma związek z programowaniem za pomocą logiki konstruktywnej. Jedno ważne zastosowanie intuicyjnej teorii zbiorów do języków programowania podał Alex Simpson, który wykorzystał ją do stworzenia syntetycznej teorii domen. Ale to dość zaawansowane rzeczy, może zobacz te slajdy . Jean-Louis Krivine opracował bardzo interesującą markę wykonalności dla klasycznej teorii zbiorów. Wydaje się to dobrym sposobem na powiązanie klasycznej teorii mnogości i programowania.
Podsumowując, teoria języków programowania wykorzystuje podstawowe techniki. Nie jest to zaskakujące, ponieważ uważamy obliczenia za podstawową koncepcję. Ale zbyt naiwne jest twierdzenie, że języki programowania są „oparte” na pewnych podstawach. W rzeczywistości trikotomia fundamentów „teoria zbiorów - teoria typów - teoria kategorii” jest po prostu użyteczną obserwacją na wysokim poziomie, którą można precyzyjnie matematycznie przedstawić na różne sposoby, ale nie ma w tym nic koniecznego. To historyczny wypadek.