Promotie: Program Sketching with Types & Examples

LET OP: De kandidaat houdt een lekenpraatje, hierdoor start de livestream een kwartier eerder.

Computerprogramma's beschrijven instructies die de computer hoort te volgen. De computer voert die maar al te graag uit, zonder daar vragen bij te stellen. Mensen maken echter vaak fouten, waardoor de computer de verkeerde dingen uitvoert. Om dit soort situaties te voorkomen, schrijven programmeurs vaak specificaties. Deze beschrijven een verwachting van de programmeur.

Dit proefschrift focust op twee veelgebruikte specificaties: tests en types. Tests beschrijven welke output de programmeur verwacht bij specifieke inputs. Types drukken de structuur van de data uit die de programmeur in diens programma verwacht. De voornaamste reden voor het schrijven van specificaties is dat de computer automatisch kan controleren of het programma aan de verwachting van de programmeur voldoet.

Het wordt vaak aangeraden om eerst specificaties te schrijven en daarna pas het programma zelf. Dit dwingt de programmeur om na te denken over diens verwachtingen én het geeft de computer de mogelijkheid om met die verwachtingen rekening te houden om de programmeur op weg te helpen. In de praktijk worden specificaties echter meestal niet ten volle benut. De computer herkent bijvoorbeeld vaak niet dat (1) de programmeur een fout heeft geïntroduceerd nog voordat het programma uitgevoerd kan worden, (2) de specificatie een contradictie bevat, of (3) er een manier is om de gaten in het programma zó te vullen dat het aan de specificatie voldoet. In dit proefschrift probeer ik deze drie punten aan te pakken om zo meer uit specificaties te kunnen halen.