Magnus Madsen

Project title

Type and Effect Inference with Boolean Algebras

What is your project about?

Software consists of source code written in a programming language. Since software developers are human, they make mistakes in their programs. The goal of this project is to develop better programming languages that can help developers catch their bugs before their programs reach end users. The key insight is to use so-called Boolean algebras to describe the computational effects that arise during the execution of a program. For example, to answer questions such as; does the program read a file from the file system? Does the program send data over the network?

How did you become interested in your particular field of research?

I was interested in programming from a young age. I started with web programming when the internet was new. Initially, I took programming languages for granted. It was only at university that it dawned on me that programming languages are designed by humans and that it is possible to design completely new languages that allow us to express computations in a new way. That was fascinating: inventing new languages to be able to express yourself better.

What are the scientific challenges and perspectives in your project?

Concretely, the project is about the development of type and effect systems that support automatic inference. This means that the programmer does not have to spend time and effort on annotating the program, but instead the programming language itself can deduce the relevant types and effects. The mathematical foundation for this idea is based on Boolean algebras which support so-called unification. This means, roughly speaking, that given two Boolean expressions, there is a unification algorithm which can calculate their most general solution - even if there are infinitely many solutions. It is this unification theory that enables us to build programming languages that have automatic type and effect inference.

What is your estimate of the impact, which your project may have to society in the long term?

My dream is that we can reach a point where software is reliable, efficient, and easy to create. My hope is that in 10-15 years our research will help ensure that most programming languages not only have type systems, but also effect systems. This will help software developers to understand and structure their programs in a sensible way and at the same time help to avoid a large number of serious programming errors.

Which impact do you expect the Sapere Aude programme will have on your career as a researcher?

The Sapere Aude grant will enable me to build a strong and internationally recognized research group within programming languages. The grant will also support our research and development of the Flix programming language (www.flix.dev) which we expect will play an important role in the spread of type and effect systems. Denmark (and Scandinavia) is internationally recognized for significant contributions to programming languages and the Sapere Aude grant will help us continue this proud tradition.

Background and personal life

I was born and raised in Brabrand in Aarhus. I first went to Gellerupskolen (now Sødalskolen) and later to HTX Christiansbjerg. It was at HTX, thanks to a group of dedicated teachers, that my interest in science was piqued. I have lived for 2 ½ years in Canada, where I worked as a postdoc at the University of Waterloo, an hour's drive from Toronto. In my spare time I like to go to the mountains (especially in the French Alps), to play badminton, to play board games with family and friends, and to take pictures.