211service.com
Garantert kode
Ariel Davis
Adam Chlipala, en førsteamanuensis i informatikk ved MIT, mener det er en bedre måte å skrive dataprogrammer på.
De fleste programmer viser bare operasjoner som datamaskinen skal utføre når den mottar bestemte typer data. Programmereren må skrive tester for å avgjøre om et program gjør det det skal, og siden det er praktisk talt umulig å forutsi alle måtene et program kan brukes på, har de fleste programvare feil.
Chlipala foretrekker såkalt funksjonell programmering. I stedet for å sette sammen imperative kommandoer, definerer en funksjonell programmerer et sett med funksjoner, eller matematiske forhold mellom innganger og utganger. I hovedsak uttrykker funksjonell programmering hva et program gjør som et sett med ligninger.
Å tenke på programmer som kombinasjoner av funksjoner kan være lite intuitivt, men for menneskene det fungerer for, er det virkelig en fantastisk produktivitetsforsterker, sier Chlipala. For det første kan det eliminere testing. Funksjonelle programmer er så matematisk presise at det er relativt enkelt å verifisere dem, eller bevise at de gjør det de skal, automatisk.
En av Chlipala hovedforskningsinteresser utvider omfanget av automatisk verifisering. For eksempel gjorde verifiseringsverktøy som han og kollegene utviklet det mulig å lage det første filsystemet – den delen av et operativsystem som styrer datalagring – garantert å ikke miste programdata under et systemkrasj.
En annen fordel med funksjonelle språk er at de eliminerer mye av gryntingsarbeidet fra programmering. Igjen, fordi funksjonelle programmer er så presise, er det enkelt for kompilatorer – programmene som gjør kode om til kjørbare filer – å finne ut hvordan de skal kjøre mest effektivt.
Et av Chlipalas mest populære verktøy er et funksjonelt språk kalt Ur/Web – det eneste programmeringsspråket som lar programmerere spesifisere alle funksjonene til en nettapplikasjon i ett enkelt program. Ur/Webs kompilator genererer deretter automatisk XML-koden, JavaScript-koden og databasespørringene som er nødvendige for å implementere applikasjonen. Det sikrer også at disse forskjellige komponentene samhandler riktig.
Ur/Web ligner på andre funksjonelle språk, men den legger til sikkerhetsfunksjoner som gjør at den automatisk kan tette hull som er vanlige i nettapplikasjoner. For eksempel kan den garantere at en del av koden importert til én del av en side (for eksempel en annonse) ikke kan spionere på en annen (for eksempel et kalenderverktøy).
Som mange informatikere i 30-årene, hadde Chlipala prøvd seg på å skrive videospill på videregående. Men den bedriften tok ham raskt i en annen retning. Da han var en førsteårsstudent, førte forsøkene hans på å skrive spill til Texas Instruments sin grafiske kalkulator til at han utviklet en kompilator for enheten.
Han fortsatte å fokusere på kompilatorer som undergraduate ved Carnegie Mellon University, og i sitt første semester som doktorgradsstudent ved University of California, Berkeley, spurte hans fremtidige oppgaverådgiver ham om han kunne tenke seg å bidra til et prosjekt om data- hjulpet verifisering. Chlipala ble umiddelbart hekta.
Det er en viss type paranoid personlighet som blir avhengig av denne typen arbeid, og det er definitivt meg, sier han. Det er ikke mange ting som er helt sikre i denne verden, men når du gjør maskinsjekkede bevis om programmer, kommer du ganske nærme.