Matematikens grundvalar och programmering av datorer Bengt Nordström, Datavetenskap, Chalmers och Göteborgs Universitet Vid slutet av 1800-talet var intresset för matematikens grunder stort. Cantor bevisade 1870 att det finns minst två slags oändligheter. Freges arbete med att hitta en solid grund för matematik punkterades av Russel som nästan omedelbart upptäckte att Freges arbete innehöll inneboende motsägelser. Hilbert föreslog att man skulle försöka hitta en metod som avgör om en matematisk sats är sann eller inte. Iden var att en sådan metod skulle följas slaviskt, inte kräva någon intelligens. Detta ledde till ett stort intresse för att studera beräkningsbarhet. Finns det något matematiskt sätt att exakt beskriva det som kan beräknas? Det är fascinerande att tänka att detta hände under 1930-talet, cirka 10 år före de första datorerna. Både Turing och von Neumann var logiker som var djupt engagerade i tillkomsten av de första datorerna. Det är ingen överdrift att säga att datorerna föddes ur vetenskapsområdet logik. Grundvalsproblem inom matematiken ledde fram till en av de viktigaste tekniska uppfinningarna. Förstår moderna forskningspolitiker detta? Datorutvecklingen har varit dramatisk, antalet komponenter i en integrerad krets har ökat från 50 komponenter år 1965 till 100 miljoner 40 år senare! Antalet datorer har ökat på motsvarande sätt. Likaså har antalet program ökat - och antalet fel i programmen! Alla som använder datorer har vant sig vid att leva med tekniskt felaktiga system. Men datorer används även i säkerhetskritiska system (kärnkraftverk, flygplan, tåg, bilar, banktransaktioner etc), system där felaktigheter leder till mänskliga katastrofer. Det traditionella sättet att övertyga sig om att ett program utför sin uppgift är att testa det. Men eftersom man bara kan testa det för vissa indata kan man aldrig vara säker på att programmet alltid fungerar. I stället måste man *bevisa* att programmet alltid löser sin uppgift. Forskningen inom datavetenskap har utvecklat program (beviseditorer, teorembevisare) med vars hjälp man kan kontrollera matematiska bevis (t.ex. om programs korrekthet). Man kan alltså med hjälp av datorer kontrollera om datorprogram alltid kommer att fungera. De tidigare teoretiska studierna av logiska formalismer har betonat intressanta matematiska egenskaper. Nu kommer man kommer man - av praktiska skäl - att utveckla logiska språk med intressanta praktiska egenskaper. Detta kommer att leda till ett ökat intresse av semantik och grundvalsproblem. På samma sätt som framsteg inom fysiken nödvändiggjorde en utveckling av matematisk analys under de senaste århundranden kommer framsteg inom datavetenskapen att nödvändiggöra en utveckling av vetenskapsområdet logik. Inom logiken kommer intresset att förflyttas från syntax till semantik och från teori till praktik. Grundvalsfrågor inom matematik och logik (t.ex. Vad är sanning?) har plötsigt blivit praktiskt viktiga. Referenser: The Types project homepage: www.cs.chalmers.se/Cs/Research/Logic/Types/