Heel veel programmatuur zit nog op het intuïtieve niveau en de meeste software wordt niet geverifieerd. Dat zit professor emeritus N.G. de Bruijn wel dwars, ook al heeft hij enig begrip voor de commerciële drijfveren van bedrijven die feitelijk onrijpe producten op de markt brengen om de concurrent voor te zijn.
|
Denkende soep
Zojuist terug van een wandelvakantie in Zwitserland ("we stegen elke dag wel zo’n vierhonderd meter") heeft de 84-jarige een leeg kamertje gevonden in het hoofdgebouw van de Technische Universiteit Eindhoven voor het gesprek. Wekelijks vertoeft hij nog steeds op het onderwijsinstituut waar hij van 1960 tot 1984 (toen hij met emeritaat ging) als professor heeft gewerkt. Hij heeft er een eigen bureau, kast en pc. "Maar het contact met studenten en medewerkers is toch wel verloren gegaan. Er is nu een andere generatie."
De zuiver wiskundige staat nog volop in het academische leven en maakt bijvoorbeeld nog opgaven voor de Nederlandse Wiskunde Olympiade, een jaarlijkse wiskundewedstrijd voor leerlingen uit de bovenbouw van de middelbare school. "Dat is erg leuk om te doen." Verder breekt hij zich nu het hoofd over ‘de denkende soep’: een fysiologisch/chemisch model voor een associatief geheugen. Dit ligt in het verlengde van zijn roaming random set-model van het geheugen dat hij heeft ontwikkeld om te bewijzen hoe een niet adresseerbaar geheugen werkt (het menselijk geheugen versus dat van een computer).
Automath
De Bruijns belangstelling voor computers voert hem naar zijn jongenstijd. "Halverwege de beklimming van de Domtoren in Utrecht zie je hoe het carillon wordt aangestuurd via een trommel met pennen. Toen dacht ik: ‘Als dit mogelijk is, kun je alles wel automatiseren’. Ik ben niet de vader van de informatica, maar ik heb wel aan de wieg gestaan."
Het eregebaar van de Nederlandse informatica hangt samen met het project Automath dat De Bruijn glans heeft gegeven. Daarvoor gaan we terug naar de beginjaren van de informatica. Eind jaren zestig is het Automath-project van de grond gekomen. Doel was een taal te ontwikkelen waarmee is na te gaan of een reeks beweringen voldoet aan de geldende wiskundige regels. "Het was toen een fantastisch groot project", zegt De Bruijn. "Er is anderhalf miljoen gulden in gegaan en het heeft vijf jaar gelopen. Na verloop van tijd wilde de ZWO (Nederlandse Organisatie voor Zuiver Wetenschappelijk Onderzoek, red.) er geen geld meer in steken. Het is toen nog voortgezet met anderhalve man en een paardenkop, maar uiteindelijk kon ik er niet mee verder. In het buitenland is het wel voortgezet, en een aantal basisideeën leeft nog steeds voort."
Uren/seconden
Gedurende het Automath-project heeft De Bruijn een test uitgevoerd. Een compleet wiskundig leerboekje is automatisch gecontroleerd op juistheid. "Dat gebeurde toen zonder softwareondersteuning", zegt hij. "Wij hadden geen invoerschermen waarop je kon zien wat je deed. Alles ging met papieren ponsbanden. Het boekje is toen in twee uur geverifieerd. Onlangs heeft de Amsterdamse wiskundige Freek Wiedijk in Nijmegen, waar hij doceert, hetzelfde leerboekje met alle coderingen opnieuw geverifieerd. Gewoon op zijn eigen pc. Hij was in twee seconden klaar. Toch was ons werk in 1970 een mijlpaal. Er wordt nog steeds aan gerefereerd."
Mag de Nijmeegse pc slechts twee seconden hebben gedaan over de verificatie, Wiedijk heeft jaren nodig gehad om in zijn vrije tijd de voorbereiding te doen. Daar zit hem de kneep. Het stoort De Bruijn dat het merendeel van de software niet wordt gecontroleerd op juistheid. Als zuiver wiskundige wil hij gewoon dat de code formeel klopt. "De moeilijkheid zit hem in de voorbereiding. Heel veel programmeurs werken nog intuïtief. Hun code is niet geformaliseerd. Dat komt dan weer omdat de industrie het onderling niet eens kan worden over notaties en regels. Toch is wat een programmeur uiteindelijk opschrijft uiterst formeel."
Slordig
Hij heeft er wel enigszins begrip voor. "Ik programmeer zelf nog steeds veel, voornamelijk om ideeën op te doen. Ik kijk wel uit om dat allemaal te verifiëren; het kost gewoon enorm veel inspanning in de voorbereiding. Bij commerciële software moet je echter andere normen aanleggen. Gelukkig, zo vernam ik laatst, is de software die regelt dat de machinistloze treinen in de Parijse metro goed rijden, wel geverifieerd."
Voort gaat het gesprek: over quasi-kristallen, zijn periode bij het Natlab van Philips, het vierkleurenprobleem, het vermoeden van Fermat, Gödel en het menselijk brein. "Ik spring van de hak op de tak", had hij al gewaarschuwd, gevolgd door die andere, typische opmerking: "ik ben meer een uitvinder dan een geleerde".< BR CLEAR=LEFT>
