Climbing Mount Everest of computer programming

Aleks Nanevski, researcher at IMDEA Software, discovered his passion for mathematics at the age of 10 when a teacher at his school in Macedonia saw his aptitude and started giving him extracurricular classes. He began to participate in regional competitions and by the age of 13 he was already on the podium in national competitions.

The mathematically gifted boy asked his parents for a computer. During a family trip to France, his parents were finally able to buy him one, the one they could afford, and Aleks began to delve into the world of programming. Unfortunately, or maybe fortunately, the instruction book for that machine was in French and he didn't know the language. For a while he also couldn't connect the computer to his TV, because of different TV standards. But the book showed example programs in the BASIC programming language along with the output of their execution. That sufficed for him to learn to program in his mind, without actually typing anything on a computer. This got him drawn into programming as an abstract mathematical activity that is independent of any computers.

His career as a researcher began with his doctorate at Carnegie Mellon University, followed by a postdoctoral position at Harvard University. He then spent a couple of years at Microsoft Research in Cambridge U.K., following which he joined IMDEA Software Institute in Madrid, where he was awarded an ERC grant worth two million euros for the project "MATHADOR: Type and Proof Structures for Concurrent Software Verification". The project, funded by the European Union’s Horizon 2020 program, has lasted 6 years and ended on March 31st. His research, as the European Research Council indicated at the time of the grant award, is high-risk because it proposes new foundations for concurrent software verification, but it is also high-gain, since concurrent software verification is one of the most important open problem in current research on programming languages and semantics.

For example, a computer program of an electric car has millions of lines of code and may work at launch, but that doesn’t mean it can't have errors. Finding the errors can be like looking for a needle in a haystack, as it involves time and resources. If, in addition, the error arises from the faulty interaction between simultaneously running components, e.g., the car connects with GPS, safety sensors or a music application, the difficulties multiply. One can consider searching for the errors in principle, but in practice this requires infeasible amount of work. To really address the problem, a radical approach is needed.

Enter functional programming and type theory; centered in the academic world, these subjects have roots in philosophy, logic, and constructive mathematics. Functional programs may not be as fast to execute as imperative programs---the ones used by software industry---but they are much easier to write and understand. An imperative program with hundreds of lines of code can often be reduced to just a few lines in the functional idiom. When programmingimperatively, we adapt to the machines. When programming functionally, we have the machines adapt to us. The idea of functional programming is to use a mathematical language that is so minimalist, concise and effective that it makes it easy to spot the programming errors, and thus not even make errors in the first place. 

Courage, patience and faith are characteristics required of someone who chooses the long path: "I started with an intuition that concurrency should fruitfully be addressed by functional programming and type theory, because I applied these previously to non-concurrent programming, which uncovered deep connections with so-called Separation Logic, an important and well-known idea in computer science. Somewhat amazingly, this intuition has so far always materialized, even when it temporarily looked like it has no chance. However, there is still a long way to the top.", according to Nanevski.

Aleks explains that his research is related to "Everything and nothing at the same time. It is a foundational problem, which implies that it is highly idealized. It takes its challenges from existing practices and technologies and removes the messiness of the real world, while striving to distill the basic core issue. That makes it related to nothing directly. But it also makes it related to everything, because that core issue is what it means for programs to interact and coordinate with each other, and this interaction arises in Artificial Intelligence, in Internet of Things, and everywhere in-between. Because of its universality, understanding the issue mathematically will open possibilities for the technologies of the future that today we can't even imagine."

“This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. [724464])”