211service.com
Garanteret kode
Ariel Davis
Adam Chlipala, lektor i datalogi ved MIT, mener, at der er en bedre måde at skrive computerprogrammer på.
De fleste programmer angiver blot operationer, som computeren skal udføre, når den modtager bestemte typer data. Programmøren skal skrive test for at afgøre, om et program gør, hvad det skal, og da det er praktisk talt umuligt at forudsige alle de måder, et program kan bruges på, har de fleste software fejl.
Chlipala foretrækker såkaldt funktionel programmering. I stedet for at sammenkæde imperative kommandoer, definerer en funktionel programmør et sæt funktioner eller matematiske forhold mellem input og output. Grundlæggende udtrykker funktionel programmering, hvad et program gør som et sæt ligninger.
At tænke på programmer som kombinationer af funktioner kan være uintuitivt, men for de mennesker, det fungerer for, er det virkelig en fantastisk produktivitetsforøger, siger Chlipala. For det første kan det eliminere test. Funktionelle programmer er så matematisk præcise, at det er relativt nemt at verificere dem, eller bevise, at de gør, hvad de skal, automatisk.
En af Chlipala's hovedforskningsinteresser udvider omfanget af automatisk verifikation. For eksempel gjorde verifikationsværktøjer, som han og kolleger udviklede, det muligt at skabe det første filsystem - den del af et operativsystem, der styrer datalagring - garanteret ikke at miste programdata under et systemnedbrud.
En anden fordel ved funktionelle sprog er, at de fjerner en masse af gryntarbejdet fra programmering. Igen, fordi funktionelle programmer er så præcise, er det nemt for compilere - de programmer, der omdanner kode til eksekverbare filer - at finde ud af, hvordan de får dem til at køre mest effektivt.
Et af Chlipalas mest populære værktøjer er et funktionelt sprog kaldet Ur/Web - det eneste programmeringssprog, der lader programmører specificere al en webapplikations funktionalitet i et enkelt program. Ur/Webs compiler genererer derefter automatisk den XML-kode, JavaScript-kode og databaseforespørgsler, der er nødvendige for at implementere applikationen. Det sikrer også, at disse forskellige komponenter interagerer korrekt.
Ur/Web ligner andre funktionelle sprog, men det tilføjer sikkerhedsfunktioner, der gør det muligt automatisk at lukke huller, der er almindelige i webapplikationer. For eksempel kan det garantere, at en smule af dens kode, der importeres til én sektion af en side (såsom en annonce), ikke kan spionere på en anden (såsom et kalenderværktøj).
Som mange dataloger i 30'erne havde Chlipala forsøgt sig med at skrive videospil i gymnasiet. Men den virksomhed tog ham hurtigt i en anden retning. Da han var en førsteårsstuderende, fik hans forsøg på at skrive spil til Texas Instruments' grafregner, ham til at udvikle en compiler til enheden.
Han fortsatte med at fokusere på compilere som bachelorstuderende ved Carnegie Mellon University, og i sit første semester som kandidatstuderende ved University of California, Berkeley, spurgte hans fremtidige specialevejleder ham, om han kunne tænke sig at bidrage til et projekt om computer- assisteret verifikation. Chlipala blev straks hooked.
Der er en vis form for paranoid personlighed, der bliver afhængig af den her slags arbejde, og det er bestemt mig, siger han. Der er ikke mange ting, der er helt sikre i denne verden, men når man laver maskintjekkede korrektur om programmer, kommer man ret tæt på.