De manier waarop we software maken is nogal onvolwassen

Het nieuwsbericht Grote fouten ontdekt in wiskundige software (NRC Handelsblad, 14 november) meldt dat er softwarefouten in Mathematica zitten, een programma dat vooral wordt gebruikt voor wetenschappelijke berekeningen.

Technisch is het mogelijk foutloze wiskundige berekeningen en bewijzen te maken. Dit kan worden bereikt door gebruik te maken van – jawel – computergestuurde bewijscheckers.

Het mooiste voorbeeld van een foutloos bewijs staat nota bene in het artikel. De vierkleurenstelling is in 1976 door Appel en Haken bewezen. In 2005 heeft Gonthier dit bewijs stap voor stap per computer gecheckt.

Waarom zijn er dan toch zoveel problemen met softwaregestuurde systemen? Dat ligt vooral aan de nogal onvolwassen manier waarop we software maken. Wat technisch kan, hoeft nog niet te worden gebruikt. Helaas, en dat is geen nieuws, geldt dat ook voor de makers van Mathematica.