Sommige wetenschappelijke ontdekkingen zijn belangrijk omdat ze iets nieuws onthullen – de dubbele spiraalvormige structuur van DNA bijvoorbeeld, of het bestaan ​​van zwarte gaten. Sommige onthullingen zijn echter diepgaand omdat ze laten zien dat twee oude concepten, waarvan men ooit dacht dat ze verschillend waren, in feite hetzelfde zijn. Neem de vergelijkingen van James Clerk Maxwell, waaruit blijkt dat elektriciteit en magnetisme twee aspecten zijn van één enkel fenomeen, of de algemene relativiteitstheorie, de koppeling van de zwaartekracht aan een gekromde ruimte-tijd.

De Curry-Howard-correspondentie doet hetzelfde, maar op grotere schaal, waarbij niet alleen afzonderlijke concepten binnen één veld, maar hele disciplines met elkaar worden verbonden: Computer Science en wiskundige logica. Ook bekend als het Curry-Howard isomorfisme (een term die betekent dat er een soort één-op-één-correspondentie bestaat tussen twee dingen), legt het een verband tussen wiskundige bewijzen en computerprogramma's.

Simpel gezegd stelt de Curry-Howard-correspondentie dat twee concepten uit de computerwetenschap (typen en programma's) respectievelijk equivalent zijn aan proposities en bewijzen: concepten uit de logica.

Eén gevolg van deze correspondentie is dat programmeren – vaak gezien als een persoonlijk ambacht – wordt verheven tot het geïdealiseerde niveau van de wiskunde. Het schrijven van een programma is niet alleen maar 'coderen', het wordt een daad van het bewijzen van een stelling. Dit formaliseert het programmeren en biedt manieren om wiskundig te redeneren over de juistheid van programma's.

De correspondentie is vernoemd naar de twee onderzoekers die het onafhankelijk hebben ontdekt. In 1934 merkte de wiskundige en logicus Haskell Curry een overeenkomst op tussen functies in de wiskunde en de implicatierelatie in de logica, die de vorm aanneemt van 'als-dan'-uitspraken tussen twee proposities.

Geïnspireerd door Curry's observatie ontdekte de wiskundige logicus William Alvin Howard in 1969 een dieper verband tussen berekeningen en logica, waaruit bleek dat het uitvoeren van een computerprogramma veel lijkt op het vereenvoudigen van een logisch bewijs. Wanneer een computerprogramma draait, wordt elke regel “geëvalueerd” om één enkele uitvoer op te leveren. Op dezelfde manier begin je bij een bewijs met complexe uitspraken die je kunt vereenvoudigen (door bijvoorbeeld overbodige stappen te elimineren of complexe uitdrukkingen te vervangen door eenvoudigere) totdat je tot een conclusie komt - een meer gecomprimeerde en beknopte bewering afgeleid van veel tussentijdse uitspraken .

Hoewel deze beschrijving een algemeen beeld geeft van de overeenkomst, moeten we, om het volledig te begrijpen, wat meer te weten komen over wat computerwetenschappers ‘typetheorie’ noemen.

Laten we beginnen met een beroemde paradox: in een dorp woont een kapper die alle mannen scheert die zichzelf niet scheren, en alleen zij. Scheert de kapper zichzelf? Als het antwoord ja is, dan mag hij zichzelf niet scheren (omdat hij alleen mannen scheert die zichzelf niet scheren). Als het antwoord nee is, moet hij zichzelf scheren (omdat hij alle mannen scheert die zichzelf niet scheren). Dit is een informele versie van een paradox die Bertrand Russell ontdekte toen hij probeerde de basis van de wiskunde te leggen met behulp van een concept dat verzamelingen wordt genoemd. Dat wil zeggen, het is onmogelijk om een ​​verzameling te definiëren die alle verzamelingen bevat die zichzelf niet bevatten, zonder tegenstrijdigheden tegen te komen.

Om deze paradox te vermijden, liet Russell zien, kunnen we ‘typen’ gebruiken. Grofweg zijn dit categorieën waarvan de specifieke waarden objecten worden genoemd. Als er bijvoorbeeld een type is met de naam 'Nat', wat natuurlijke getallen betekent, zijn de objecten 1, 2, 3, enzovoort. Onderzoekers gebruiken doorgaans een dubbele punt om het type object aan te duiden. Het getal 7, van het type geheel getal, kan worden geschreven als ‘7: geheel getal’. Je kunt een functie hebben die een object van type A neemt en een object van type B uitspuugt, of een functie die een paar objecten van type A en type B combineert tot een nieuw type, genaamd 'A × B'.

Eén manier om de paradox op te lossen is daarom deze typen in een hiërarchie te plaatsen, zodat ze alleen elementen van een ‘lager niveau’ kunnen bevatten dan zijzelf. Dan kan een type zichzelf niet in bedwang houden, waardoor de zelfreferentialiteit wordt vermeden die de paradox creëert.

In de wereld van de typetheorie kan het bewijzen dat een bewering waar is er anders uitzien dan we gewend zijn. Als we willen bewijzen dat het gehele getal 8 even is, dan is het een kwestie van laten zien dat 8 inderdaad een object is van een specifiek type genaamd 'Even', waarbij de regel voor lidmaatschap deelbaar is door 2. Nadat we hebben geverifieerd dat 8 deelbaar is bij 2 kunnen we concluderen dat 8 inderdaad een “inwoner” is van het type Even.

Curry en Howard lieten zien dat typen fundamenteel gelijkwaardig zijn aan logische proposities. Wanneer een functie een type 'bewoont' - dat wil zeggen, wanneer je met succes een functie kunt definiëren die een object van dat type is - laat je effectief zien dat de overeenkomstige stelling waar is. Functies die een invoer van type A aannemen en een uitvoer van type B geven, aangeduid als type A → B, moeten dus overeenkomen met een implicatie: "Als A, dan B." Neem bijvoorbeeld de stelling: 'Als het regent, is de grond nat.' In de typetheorie zou deze stelling worden gemodelleerd door een functie met het type 'Raining → GroundIsWet'. De verschillend ogende formuleringen zijn in feite wiskundig hetzelfde.

Hoe abstract deze koppeling ook mag klinken, het heeft niet alleen de manier veranderd waarop beoefenaars van wiskunde en informatica over hun werk denken, maar heeft ook geleid tot verschillende praktische toepassingen op beide terreinen. Voor de informatica biedt het een theoretische basis voor softwareverificatie, het proces waarbij de juistheid van software wordt gegarandeerd. Door gewenst gedrag in termen van logische proposities te kaderen, kunnen programmeurs wiskundig bewijzen dat een programma zich gedraagt ​​zoals verwacht. Het biedt ook een sterke theoretische basis voor het ontwerpen van krachtigere functionele programmeertalen.

En voor de wiskunde heeft de correspondentie geleid tot de geboorte van bewijs assistenten, ook wel interactieve stellingbewijzers genoemd. Dit zijn softwaretools die helpen bij het maken van formele bewijzen, zoals Coq en Lean. In Coq is elke stap van het bewijs in wezen een programma, en de geldigheid van het bewijs wordt gecontroleerd met typecontrole-algoritmen. Wiskundigen hebben ook bewijsassistenten gebruikt, met name de Bewijzer van de magere stelling — het formaliseren van de wiskunde, wat inhoudt dat wiskundige concepten, stellingen en bewijzen in een rigoureus, computerverifieerbaar formaat worden weergegeven. Daardoor kan de soms informele taal van de wiskunde door computers worden gecontroleerd.

Onderzoekers onderzoeken nog steeds de gevolgen van deze link tussen wiskunde en programmeren. De oorspronkelijke Curry-Howard-correspondentie combineert programmeren met een soort logica die intuïtionistische logica wordt genoemd, maar het blijkt dat meer soorten logica ook voor dergelijke unificaties vatbaar zouden kunnen zijn.

“Wat er in de eeuw sinds Curry’s inzicht is gebeurd, is dat we steeds meer gevallen ontdekken waarin ‘logisch systeem X correspondeert met computersysteem Y’”, zegt Michaël Clarkson, een computerwetenschapper aan de Cornell University. Onderzoekers hebben programmeren al in verband gebracht met andere soorten logica, zoals lineaire logica, waaronder het concept van ‘hulpbronnen’, en modale logica, die zich bezighoudt met concepten van mogelijkheid en noodzaak.

En hoewel deze correspondentie de namen van Curry en Howard draagt, zijn zij zeker niet de enigen die het hebben ontdekt. Dit getuigt van het fundamentele karakter van de correspondentie: mensen blijven het keer op keer opmerken. "Het lijkt geen toeval dat er een diepgaand verband bestaat tussen berekeningen en logica", zegt Clarkson.