Freek Wiedijk:Computers zijn heel bijzondere objecten

Ik vind computers heel bijzondere objecten. Laat ik proberen te analyseren waarom ik ze zo spannend vind. De belangrijkste redenen die ik zo kan bedenken zijn:

1. Computers zijn de meest complexe van alle menselijke maaksels.
   (Ik weet niet of dit zo is, maar het zou me niets verbazen.) Als ik naar computers kijk ervaar ik in ieder geval een zeer complex, gelaagd geheel, van een complexiteit die dat van een biologische organisme benadert. De gelaagdheid zoals die in bijv. Tanenbaum's boek wordt behandeld (de processor met zijn microcode en pipelines en "multiple cores" en wat niet daar dan omheen het geheugen en een buitenwereld van interfaces die met die processor communiceert, en daarbovenop het OS met zijn veelheid aan abstracties die het aan de programmatuur daarboven aanbiedt) is in het bijzonder fascinerend. Een computer is een zeer complex artefact waarbij alle onderdelen (vrijwel) naadloos in elkaar passen. Dat vindt ik heel mooi.
2. Computers zijn pure abstractie
   Computers zijn gemaakt van wiskunde. Helemaal onderaan, op het niveau van de logische poorten, heb je nog iets van de "fuzziness" van de natuur, maar direct daarboven wordt het volledig abstract. Deze 'netheid' vind ik zeer aantrekkelijk. Het is als het verschil tussen een handgeschreven brief en eentje die in een tekstverwerker zit: de laatste is volledig "netjes". Die netheid, die puurheid trekt me zeer aan.
3. Computers geven je iets voor niets
   Dat vind ik het wonder van computerprogramma's. Je hebt een vraag, je programmeert tien minuutjes (of tien jaar), je voert het programma dat je hebt gemaakt uit, en verdomd, er komt iets uit wat je zonder de computer nooit gehad had. Een oplossing van een puzzel, een mooi plaatje, een accuratere weersvoorspelling dan je zonder computer had gehad, etc. Het komt op mij altijd als een wonder over.
4. Computers zijn zeer ambachtelijk.
   Het werken met computers (en in het bijzonder het programmeren) is heel duidelijk een ambacht. Het is geen kennis, het is een kunde. Bij computers //maak// je iets, het is een heel creatief vak. Je leert het ook niet echt goed uit een boek of in een college: je leert de echt belangrijke dingen meestal van iemand anders, door osmose. Althans, zo werkte het bij mij. Er is echt vaak sprake van een meester/gezel relatie. Dat ambachtelijke, dat vind ik heel aantrekkelijk.

Een andere manier om iemand te vragen wat hij of zij fascinerend aan informatica vindt, is te vragen wat iemands favoriete informatica-boeken zijn. Hierbij een tiental favorieten van mijn informatica-plankje:

1. Knuth's the Art of Computer Programming
2. Tanenbaum's Structured Computer Organization
3. Hennesy & Patterson over Computer Architecture
4. Harrison's Theorem Proving with the Real Numbers
5. Nielsen & Chuang, Quantum Computation & Quantum Information
6. Laurel, The Art of Human-Computer Interface Design
7. Jones & Lins, Garbage Collection
8. Golberg e.a., de Smalltalk-80 boeken
9. Wulf e.a., The Design of an Optimizing Compiler
10. Lions' commentaar op de Unix 6th Edition source code

Wat betreft mijn eigen onderzoek/onderwijs, heb ik geen makkelijk uit te leggen voorbeeld van iets spannends dat met bewijsformalisatie te maken heeft. Evenwel heb ik wel een verhaaltje:

Enige jaren geleden zat ik een project waarin we intensief formaliseerden. Het aardige van formaliseren (het in de computer coderen van een wiskundig bewijs) is dat het heel verwant is aan computerprogrammeren, maar dat je weet dat er geen fouten in je "programma" kunnen zitten, omdat de correctheid (de hele correctheid) door de computer wordt gecontroleerd.
Toen dit project klaar was, en ik weer eens aan een "gewoon" computerprogramma werkte, gaf dat een heel onzeker gevoel. Er konden plotseling weer "bugs" zijn! Ik was gewend was geraakt aan totaal correcte "software", en het was een heel griezelige ervaring plotseling zelf weer voor de correctheid verantwoordelijk te zijn. Het was alsof in een circus het vangnet plotseling was verwijderd.
Nu zal iemand met enige programmeerervaring zich in de eerste plaats al niet kunnen voorstellen dat het mogelijk is om er zeker van te kunnen zijn dat een programma foutloos is. ("Software zonder bugs bestaat niet.") Daarom vind ik deze ervaring die ik had - dat dit inderdaad mogelijk is, met bewijsassistenttechnologie - zo bijzonder.