Magiska och matematiska vägar till korrekt mjukvara

Bild

Nycklar till felfri mjukvara

Professor Thierry Coquands forskning rör sig i gränslandet mellan matematisk logik och teoretisk datavetenskap. Ett av Thierrys stora intressen handlar om att skapa bevissystem som kan kontrollera korrektheten i matematiska bevis. Precis samma teknik kan sedan användas för att kontrollera korrektheten i programvara.

Området kan verka abstrakt och svårtillgängligt, men är samtidigt extremt viktigt – både ur matematisk och datavetenskaplig synvinkel. Att hitta effektiva metoder för att säkerställa att mjukvaran i vårt samhälle fungerar korrekt är grundläggande för att vår civilisation ska fungera. Det handlar om allt från att flyg ska kunna lyfta och landa till tillförlitliga banktransaktioner, att vi kan göra inköp på nätet, att programvaran i bilen inte kraschar och att våra betalkort fungerar. Kort sagt en oändlig lista.

Forskning med anor från Bertrand Russel

Forskningen inom Thierrys Coquands område typteori sträcker sig tillbaka till runt 1900 då filosofen och matematikern Bertrand Russell uppfann begreppet types för att lösa ett antal matematiska problem. Vid den här tiden handlade området enbart om problemlösning inom den grundläggande matematiken. Typteori kom så småningom att bli den mest exakta formuleringen av logik och långt senare att även innefatta kopplingar mellan matematiska bevis och datorprogram.

Oändligt många användningsområden

Typteori är ett område med oändliga möjligheter där spektrumet över tänkbara tillämpningar för tekniken nästan inte går att överblicka.

Thierrys Coquands idéer kring hur man kontrollerar exaktheten i matematiska bevis bidrog under sent 90-tal till att bevissystemet Coq utvecklades i Frankrike. Något senare använde forskare vid Microsoft Research i Paris systemet för att formalisera det berömda problemet och beviset fyrfärgsteoremet.

Typteori används också inom institutionens forskning på området språkteknologi, eftersom en typ fungerar som bärare av innebörd. Vid översättning mellan olika språk blir typerna det mellanled som resulterar i att översättningarna får en korrekt grammatik.

Thierry Coquand berättar om sitt senaste ERC Advanced Grant och forskningen bakom:

– Det är ett mycket spännande forskningsområde som jag genom ERC-anslaget nu får möjlighet att fördjupa mig ytterligare inom. Min forskning rör sig i området abstrakt matematik där målet är att kunna kontrollera matematiska bevis och även de datorprogram som bygger på abstrakt matematik, till exempel olika krypteringsprogram, säger Thierry Coquand.

– Finessen är att vi använder programvara för att verifiera programvara. Vi betraktar indata och utdata i ett datorprogram som matematiska objekt och kan då ställa en rent matematisk exakt fråga om deras korrekthet. Representationerna av matematiska objekt används både för att designa interaktiva bevissystem där matematiker och datavetare får hjälp att konstruera matematiska bevis – och sedan även för att säkerställa att beviset är korrekt.

Mycket svårt att kontrollera att
ett datorprogram verkligen räknar rätt

Upptäckt som revolutionerade området

– Medan jag arbetade med mitt första ERC-projekt upptäckte den briljante men tyvärr nu bortgångne matematikern Vladimir Voevodsky att språket vi använde för att representera bevis på en dator faktiskt var väl anpassat för att uttrycka nya abstrakta begrepp i matematik. Lösningen är kopplad till begreppet homotopi, som är en studie av begreppet former.

– Dagens bevissystem är avancerade, men innan Vladimir Voevodsky lyckades hitta en lösning var det inte klart hur vissa nutida abstrakta matematiska begrepp skulle hanteras i bevissystemen. Hans resultat var både överraskande och spännande och i olika projekt försöker jag och mina kollegor nu undersöka kopplingarna vidare och designa bevissystem där abstrakta matematiska begrepp och beräkningar uttrycks på ett enhetligt sätt.

Viktigt för mjukvarans korrekthet – till
exempel inom kryptering eller flygelektronik

– Det här är användbart på många sätt. Inom områden som kryptering används mycket abstrakta matematiska objekt. Om vi ska kunna bevisa att de algoritmer som används för krypteringen är korrekta, måste vi först ha en teknik för att uttrycka de matematiska begreppen i bevissystemen. Metoden har med framgång också använts när det gäller att kontrollera mjukvara som används i flygelektronik.

– Det har länge funnits ett mycket stort och kontinuerligt växande behov av system som kan kontrollera och dokumentera komplexa mjukvarusystem, men även matematiska bevis. En aspekt av forskningen som jag personligen tycker är särskilt intressant är att arbetet med att representera matematik på en dator tvingar oss att tänka på varje matematiskt objekts natur.

– Forskningsfältet är med andra ord mycket viktigt både för civilsamhället – säker och korrekt mjukvara är avgörande för en otroligt stor mängd samhällsfunktioner idag – men också genom de möjligheter det skapar för området logik. Om projektet lyckas kommer vi att kunna skapa bevissystem som både kan bidra till vidareutvecklingen av sofistikerad matematik och också till utvecklingen av ett mycket brett spektrum av olika mjukvarusystem.

– Den här forskningen är verkligen ett lagarbete, både lokalt och internationellt. Det är väldigt roligt och känns också privilegierat att få vara en del av ett team som har så stor kompetens både i teorin och även i själva implementeringen av bevissystemen. Jag vill också tacka Forsknings- och innovationskontoret vid Göteborgs universitet, särskilt Maria Enge, för all hjälp.

Text: Catharina Jerkbrant