Al twintig jaar bestaat er een methode om te bewijzen dat er geen bugs in dat soort pointerprogramma’s zitten: separatielogica. Een fundamenteel onderzoeksgebied met veel toepassingen in de praktijk. Hiep: ‘Als je als printerfabrikant wilt dat Microsoft automatisch jouw printers herkent, moet je bijvoorbeeld eerst kunnen aantonen dat de software van die printers geen gevaar is voor hun besturingssysteem. Dat gebeurt met separatielogica. Ook Facebook maakt er veel gebruik van. Daar zijn duizenden programmeurs in dienst die, met behulp van AI, non-stop analyseren of er geen fouten in de programmatuur staan. En hoe werkt die AI? Met separatielogica.’
Een gapend gat, dat wil niet iedereen horen
Separatielogica is dus een manier om fouten in computerprogramma’s te vinden. Maar Hieps onderzoek gaat nog een niveau hoger, legt hij uit. ‘Het richt zich op het vinden van fouten in dat bewijssysteem, in de separatielogica zelf.’ Het is niet zo dat het huidige systeem incorrect is. ‘Dat wil zeggen: als je een formule bewijst, dan is het wel degelijk waar. Alleen ik heb ontdekt dat er ook ware formules zijn die je met deze logica niet kon bewijzen. Je hebt dus een onvolledig bewijssysteem dat zelf wel correct is, maar niet alles kan bewijzen dat waar is.’
Je zou het een gapend gat in de bewijslast kunnen noemen. En dat vond niet iedereen even leuk om te horen. Hiep: ‘Als je al tijden werkt in dit onderzoeksgebied, of je hebt er als bedrijf miljoenen ingestopt, is het niet leuk als een promovendus komt vertellen dat het niet klopt. Het kostte daarom best veel moeite om mijn artikelen te publiceren. Maar het is gelukt.’
