211service.com
Garanterad kod
Ariel Davis
Adam Chlipala, docent i datavetenskap vid MIT, tycker att det finns ett bättre sätt att skriva datorprogram.
De flesta program listar bara operationer som datorn ska utföra när den tar emot särskilda typer av data. Programmeraren måste skriva tester för att avgöra om ett program gör vad det ska, och eftersom det är praktiskt taget omöjligt att förutsäga alla sätt ett program kan användas på, har de flesta program buggar.
Chlipala föredrar så kallad funktionell programmering. Istället för att sammanfoga imperativa kommandon, definierar en funktionell programmerare en uppsättning funktioner, eller matematiska relationer mellan ingångar och utgångar. Funktionell programmering uttrycker i huvudsak vad ett program gör som en uppsättning ekvationer.
Att tänka på program som kombinationer av funktioner kan vara ointuitivt, men för människorna det fungerar för är det verkligen en fantastisk produktivitetshöjare, säger Chlipala. För det första kan det eliminera testning. Funktionella program är så matematiskt exakta att det är relativt enkelt att verifiera dem, eller bevisa att de gör vad de ska, automatiskt.
En av Chlipalas huvudsakliga forskningsintressen utvidgar räckvidden för automatisk verifiering. Till exempel gjorde verifieringsverktyg som han och kollegor utvecklade det möjligt att skapa det första filsystemet – den del av ett operativsystem som styr datalagring – som garanterat inte förlorar programdata under en systemkrasch.
En annan fördel med funktionella språk är att de eliminerar mycket av grymtandet från programmering. Återigen, eftersom funktionella program är så exakta, är det lätt för kompilatorer – de program som omvandlar kod till körbara filer – att ta reda på hur de ska köras mest effektivt.
Ett av Chlipalas mest populära verktyg är ett funktionellt språk som kallas Ur/Web – det enda programmeringsspråket som låter programmerare specificera alla funktioner i en webbapplikation i ett enda program. Ur/Webs kompilator genererar sedan automatiskt XML-koden, JavaScript-koden och databasfrågorna som krävs för att implementera applikationen. Det säkerställer också att dessa olika komponenter interagerar korrekt.
Ur/Web liknar andra funktionella språk, men det lägger till säkerhetsfunktioner som gör det möjligt att automatiskt täppa till hål som är vanliga i webbapplikationer. Till exempel kan det garantera att en del av dess kod som importeras till en del av en sida (som en annons) inte kan spionera på en annan (som ett kalenderverktyg).
Liksom många datavetare i 30-årsåldern hade Chlipala försökt sig på att skriva tv-spel på gymnasiet. Men det företaget tog honom snabbt i en annan riktning. När han var nybörjare ledde hans försök att skriva spel för Texas Instruments grafräknare att han utvecklade en kompilator för enheten.
Han fortsatte att fokusera på kompilatorer som grundutbildning vid Carnegie Mellon University, och under sin första termin som doktorand vid University of California, Berkeley, frågade hans framtida avhandlingsrådgivare honom om han ville bidra till ett projekt om dator- understödd verifiering. Chlipala blev omedelbart hooked.
Det finns en viss typ av paranoid personlighet som blir beroende av den här typen av arbete, och det är definitivt jag, säger han. Det finns inte många saker som är helt säkra i den här världen, men när du gör maskinkontrollerade korrektur om program kommer du ganska nära.