211service.com
Gegarandeerde code
Ariel Davis
Adam Chlipala, universitair hoofddocent computerwetenschappen aan het MIT, denkt dat er een betere manier is om computerprogramma's te schrijven.
De meeste programma's vermelden alleen bewerkingen die de computer moet uitvoeren wanneer deze bepaalde soorten gegevens ontvangt. De programmeur moet tests schrijven om te bepalen of een programma doet wat het moet doen, en aangezien het vrijwel onmogelijk is om alle manieren te voorspellen waarop een programma kan worden gebruikt, bevat de meeste software bugs.
Chlipala geeft de voorkeur aan zogenaamd functioneel programmeren. In plaats van dwingende commando's aan elkaar te rijgen, definieert een functionele programmeur een reeks functies of wiskundige relaties tussen inputs en outputs. Functioneel programmeren drukt in wezen uit wat een programma doet als een reeks vergelijkingen.
Programma's zien als combinaties van functies kan niet intuïtief zijn, maar voor de mensen waarvoor het werkt, is het echt een geweldige productiviteitsverbeteraar, zegt Chlipala. Om te beginnen kan het testen elimineren. Functionele programma's zijn zo wiskundig nauwkeurig dat het relatief eenvoudig is om ze te verifiëren, of te bewijzen dat ze automatisch doen wat ze zouden moeten doen.
Een van Chlipala's? belangrijkste onderzoeksinteresses breidt de reikwijdte van automatische verificatie uit. De verificatietools die hij en collega's ontwikkelden, maakten het bijvoorbeeld mogelijk om het eerste bestandssysteem te creëren - het deel van een besturingssysteem dat de gegevensopslag regelt - dat gegarandeerd geen programmagegevens kwijtraakt tijdens een systeemcrash.
Een ander voordeel van functionele talen is dat ze een groot deel van het programmeerwerk elimineren. Nogmaals, omdat functionele programma's zo nauwkeurig zijn, is het gemakkelijk voor compilers - de programma's die code omzetten in uitvoerbare bestanden - om erachter te komen hoe ze het meest efficiënt kunnen werken.
Een van Chlipala's meest populaire tools is een functionele taal genaamd Ur/Web, de enige programmeertaal waarmee programmeurs alle functionaliteit van een webtoepassing in één programma kunnen specificeren. De compiler van Ur/Web genereert vervolgens automatisch de XML-code, JavaScript-code en databasequery's die nodig zijn om de toepassing te implementeren. Het zorgt er ook voor dat deze verschillende componenten correct samenwerken.
Ur/Web is vergelijkbaar met andere functionele talen, maar het voegt beveiligingsfuncties toe waarmee het automatisch gaten kan dichten die veel voorkomen in webtoepassingen. Het kan bijvoorbeeld garanderen dat een deel van zijn code die in een gedeelte van een pagina is geïmporteerd (zoals een advertentie) een ander gedeelte niet kan bespioneren (zoals een kalendertool).
Zoals veel computerwetenschappers van in de dertig, had Chlipala op de middelbare school geprobeerd videogames te schrijven. Maar die onderneming bracht hem al snel in een andere richting. Toen hij een eerstejaarsstudent was, leidden zijn pogingen om spellen te schrijven voor de grafische rekenmachine van Texas Instruments hem ertoe een compiler voor het apparaat te ontwikkelen.
Hij bleef zich concentreren op compilers als student aan de Carnegie Mellon University, en in zijn eerste semester als afgestudeerde student aan de University of California, Berkeley, vroeg zijn toekomstige scriptieadviseur hem of hij zou willen bijdragen aan een project over computer- ondersteunde verificatie. Chlipala was meteen verkocht.
Er is een bepaald soort paranoïde persoonlijkheid die verslaafd raakt aan dit soort werk, en dat ben ik zeker, zegt hij. Er zijn niet veel dingen die absoluut zeker zijn in deze wereld, maar als je machinaal gecontroleerde bewijzen over programma's doet, kom je redelijk dichtbij.