Turingsprisen for 2013 er tildelt Leslie Lamport, en forskningsleder ved Microsoft Research. Dette kunngjorde ACM (Association for Computing Machinery) denne uken.

Prisen, som av mange regnes som en slags Nobelpris innen databehandling, gis til Lamport for hans bidrag til å påtvinge klar og veldefinert sammenheng i den tilsynelatende kaotiske atferden til distribuerte datasystemer, hvor flere autonome datamaskiner kommuniserer ved å sende hverandre meldinger.

Ifølge ACM har Lamport tenkt ut flere viktige algoritmer og utviklet formelle protokoller for modellering og verifisering, noe som forbedret kvaliteten til virkelig distribuerte systemer. Bidragene skal ha ført til å bedre nøyaktigheten, ytelsen og påliteligheten til datasystemer.

– Som en anvendt matematiker hadde Leslie Lamport en ekstra bevissthet for hvordan å bruke matematiske verktøy på viktige, praktiske problemer. Ved å finne nyttige måter for å skrive spesifikasjoner og å bevise riktigheten til realistiske algoritmer – noe som sørger for et sterkt fundament for komplekse dataoperasjoner – bidro han til å flytte verifiseringen fra å være en akademisk disiplin til bli et praktisk verktøy, sier Vint Cerf, som er president i ACM, i en pressemelding.

Lamports algoritmer og verktøy er mye brukt, blant annet innen sikkerhet, nettskyløsninger, integrerte systemer, databasesystemer og oppgavekritiske datasystemer som avhenger av sikker informasjonsdeling og -interoperabilitet for å unngå feil.

Ifølge ACM har Lamport bidratt til påliteligheten og robustheten ved design av både programvare- og maskinvareteknologi med sine ideer om «safety», hvor det ikke skjer noe galt, og «liveness», hvor det skjer noe godt.

Lamport skal også ha kommet med løsninger for bysantinsk feiltoleranse, som bidrar til å hindre feil i systemkomponenter som opptrer feilaktig når den samhandler med andre komponenter.

LaTeX
Mange informatikere kjenner kanskje Lamport som oppfinneren av LaTeX, som fortsatt regnes som de facto-standarden for teknisk publisering innen blant annet informatikk. Det er kanskje nettopp derfor at ACM har generert en PDF-versjon av pressemeldingen med LaTeX.

Lamport skapte i sin tid også språket TLA+ for temporal-logikk, som ifølge ACM bidrar ved skriving av nøyaktige og robuste spesifikasjoner.

– Hans pionerarbeid innen distribuerte og samvirkende algoritmer har i vesentlig grad forbedret både forbrukerrettede og industrielle datasystemer, fra multiprosessorteknologi i datasentraler til multidatamaskin-nettverk brukt i kontrollsystemer for luftfart, sier Wen-Hann Wang, daglig leder for Intel Labs, i pressemeldingen.

– Spesielt har den strålende «logical clock»-abstraksjonen, som han introduserte for omtrent 40 år siden, hatt en enorm innvirkning på feltet. Den bidro med et elegant rammeverk for resonnementer om distribuerte protokoller, noe som er kritiske elementer i den sammenkoblede verdenen.

Turingsprisen, eller «ACM A.M. Turing Award» som den offisielt heter, inkluderer en pengesum på 250 000 dollar. Prisen finansieres av Intel og Google. Den vil bli overrakt under en bankett i San Francisco i juni.

Lamport har tidligere vært ansatt i SRI International og Digital Equipment Corporation (DEC). Han er tatt sine universitetsgrader i matematikk ved Massachusetts Institute of Technology og Brandeis University.

Microsoft har i anledningen publisert en lang artikkel om Leslie Lamport her.