Magnus Madsen

Projekttitel

Type and Effect Inference with Boolean Algebras

Hvad handler dit projekt om?

Software består af kildekode skrevet i et programmeringssprog. Da softwareudviklere er mennesker kommer de fra tid til anden til at lave fejl i deres programmer. Målet med dette projekt er at udvikle bedre programmeringssprog som kan hjælpe udviklere med at fange deres fejl, før deres programmer kommer ud til slutbrugerne. Den gode idé er at bruge såkaldte Boolske algebraer til at beskrive beregningsmæssige effekter under udførslen af et program. Det kunne være for at besvare spørgsmål som f.eks. læser programmet en fil fra filsystemet? Sender programmet data over netværket?

Hvordan opstod din interesse for dit forskningsfelt?

Jeg var fra en ung alder interesseret i programmering. Jeg startede med web-programmering, den gang internettet var nyt. Oprindeligt tog jeg programmeringssprog for givet. Det var først på universitetet, at det gik op for mig, at programmeringssprog er designet af mennesker, og at det er muligt at designe helt nye sprog, som tillader os at udtrykke beregninger på en ny måde. Dét var fascinerende: at opfinde nye sprog for at kunne udtrykke sig bedre.

Hvad er de forskningsmæssige udfordringer og perspektiver ved dit projekt?

Konkret handler projektet om udvikling af type og effekt systemer, som understøtter automatisk inferens. Det vil sige, at programmøren ikke skal bruge tid og kræfter på at annotere programmet, men i stedet kan programmeringssproget selv deducere de relevante typer og effekter. Det matematiske fundament for denne ide bygger på Boolske algebraer, som understøtter såkaldt unificering. Det betyder, groft sagt, at givet to Boolske udtryk så findes der en unificerings-algoritme som kan beregne deres mest-generelle løsning - også selvom der er uendeligt mange løsninger. Det er denne unificerings-teori som muliggør, at vi kan bygge programmeringssprog, som har automatisk type og effekt inferens.

Hvilke perspektiver vurderer du selv, at din forskning på sigt kan have for det omgivende samfund?

Min drøm er, at vi kan nå til et punkt, hvor software er pålideligt, effektivt og nemt at skabe. Mit håb er, at om 10-15 år vil vores forskning være med til at sikre, at de fleste programmeringssprog ikke kun har typesystemer, men også effektsystemer. Dette vil hjælpe softwareudviklere med at forstå og strukturere deres programmer på en fornuftig måde og samtidigt hjælpe med at undgå en lang række alvorlige programmeringsfejl.

Hvad vil det betyde for din forskerkarriere, at du indgår i Sapere Aude-programmet?

Sapere Aude-bevillingen vil gøre mig i stand til at opbygge en stærk og internationalt anerkendt forskningsgruppe indenfor programmeringssprog. Bevillingen vil endvidere understøtte vores forskning og udvikling af Flix programmeringssproget (www.flix.dev), som vi forventer, vil spille en vigtig rolle i udbredelsen af type og effekt systemer. Danmark (og Skandinavien) er internationalt anerkendt for væsentlige bidrag til programmeringssprog, og Sapere Aude-bevillingen vil være med til, at vi kan fortsætte denne stolte tradition.

Lidt om mennesket bag forskeren

Jeg er født og opvokset i Brabrand i Aarhus. Jeg gik først på Gellerupskolen (nu Sødalskolen) og senere på HTX Christiansbjerg. Det var på HTX, takket være en række dygtige undervisere, at min interesse for naturvidenskab blev vækket. Jeg har boet 2 ½ år i Canada, hvor jeg arbejdede som postdoc på University of Waterloo en times kørsel fra Toronto. I min fritid kan jeg godt lide at gå i bjergene (især i de franske alper), at spille badminton, at spille brætspil med familie og venner og at tage billeder.