Aleks Nanevski has dedicated his life to solving one of the biggest computer science challenges, taking a long and risky road towards revolutionizing how we think about programming in general, and concurrent programming specifically.
IMDEA Software Institute researcher Aleks Nanevski was awarded an ERC grant for “MATHADOR: Type and Proof Structures for Concurrent Software Verification in April 2017 worth €2 million. 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.
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 programming imperatively, 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.
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.”
“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.
“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])”
