Softwarebugs kunnen leiden tot kostbare of zelfs gevaarlijke fouten. Hoe kunnen we garanderen dat een computerprogramma werkt zoals bedoeld? Met testen alleen kunnen we niet alle fouten uitsluiten. Vereist zijn: (1) een nauwkeurige definitie van wat het programma precies dient te doen (een specificatie) en (2) een wiskundig bewijs dat het programma aan die specificatie voldoet. Computerprogramma’s en bewijzen zijn doorgaans complex, dus deze twee zaken vereisen een precieze en verfijnde taal. Typentheorie is zo’n taal. Om uiteindelijk de verificatie van programma’s en bewijzen te bevorderen, zal dit project typentheorie uitbreiden met wiskundige instrumenten uit de categorieëntheorie.
