Softwaretesten of formele verificatie – waarom wiskundig bewijs doorslaggevend is

In dit fragment uit Elektor Engineering Insights #54 stelde ik Quentin Ochem van AdaCore de voor de hand liggende maar irritante vraag: waarom kunnen we niet gewoon overal softwaretests op loslaten en klaar zijn?

Zoals Quentin opmerkt, zou zelfs een piepkleine functie met twee gehele getallen een astronomisch aantal testgevallen vereisen om alle mogelijkheden af te dekken. Je zou testen tot aan de hitte-dood van het universum en toch nog iets missen. Coverage-metrics, fuzzing, grensanalyse — ze helpen allemaal, maar geen ervan kan correctheid bewijzen.
 

Formele verificatie daarentegen kan dat wel. Met SPARK kun je wiskundig bewijzen dat je code precies doet wat de specificatie zegt, in 100% van de gevallen. Dat niveau van zekerheid is misschien overdreven in veiligheidskritische contexten, waar “negen negens” betrouwbaarheid goed genoeg kan zijn, afhankelijk van de kosten. Maar in beveiliging hebben aanvallers slechts één exploit nodig in tien miljoen regels code, dus bewijs wint altijd van waarschijnlijkheid.

Quentin mijmerde ook over AI die zich bij het feest aansluit — niet ter vervanging van statische analyzers, maar als aanvulling, met nieuwe manieren om bugs op te sporen en misschien zelfs oplossingen aan te dragen. Ik zei hem dat ik het pas geloof als mijn IDE ophoudt me lastig te vallen over ontbrekende puntkomma’s.
 

Wat denkt u? Softwaretesten vs. formele verificatie

Formele verificatie klinkt misschien als academische overdaad, maar Quentins punt is duidelijk: wanneer aanvallers maar één bug hoeven te vinden, zijn de kansen tegen je als je uitsluitend op testen vertrouwt. Tools als SPARK verschuiven de discussie van waarschijnlijkheid naar zekerheid, en dat roept vragen op voor iedereen die code schrijft — van embedded engineers tot softwareteams die voortdurend onder druk staan om te leveren. Ik hoor graag wat u denkt: is bewijs de toekomst, of nemen de meesten van ons genoegen met “genoeg getest”? Deel uw mening in de reacties.