“Programs are mathematics turned into physics”
ETH Zurich professor Ralf Jung is on a mission to create a world in which buggy software is a thing of the past. His tools for achieving that goal are also his biggest intellectual passions: mathematics and logic.
A world without software bugs: that’s the simple, albeit exceedingly hard-to-achieve goal of Ralf Jung’s research. As recent events have once more made apparent, faulty programs can bring large chunks of the world’s economy grinding to a halt. In the worst case, malfunctioning code can cost human lives (Therac-25, for example). And it’s hard to predict when the next catastrophic error will hit, as our reliance on potentially flawed technology keeps growing.
“It’s insanely frustrating, because computer programs are as close as we have to the perfection of Platonic ideas. Programs are basically maths turned into physics, and maths is supposed to be rigorous, reproducible, deterministic,” says Jung.
Jung bemoans that reality looks very different from the ideal, though. Programs crash all the time, and people have gotten used to it. “The closer you look into programs, the more you wonder why anything works at all. It’s a pure miracle,” says Jung.
An astonishing insight
Jung’s field of research is in formal methods for software verification. In contrast to techniques such as software testing, which check for performance, reliability and correctness of programs in a limited number of situations, formal methods aim to prove – with the rigorous tools of mathematics and logic – certain properties of software or even entire programming languages.
The goal is to assert whether computer programs will crash, whether they’ll produce the expected outputs or whether there’ll be an output at all after the program has executed – and these assertions must always be true. It’s a line of work that combines the intellectual pursuits closest to Jung’s heart.
“Discovering that there’s such a deep connection between logic and programming was one of my life’s biggest moments,” says Jung. It’s a revelation for which he credits his long-time mentor Gert Smolka, a professor of computer science at Saarland University in Germany. Jung rates Smolka’s course “Introduction to Computational Logic”, which he took as an undergrad, as the single most influential experience he had during his formative years. “I had always loved both logic and programming, and Smolka, who was a very enthusiastic lecturer, taught me that they were, on a profound level, the same thing. It was absolutely mind-boggling” Jung recalls.
Mathematics on the run
Jung’s love affair with maths has its roots in his early childhood. Recreational maths would constantly come up in dinner-table conversations. His parents, both scientists with doctoral degrees, would pose him and his younger brother math puzzles to keep the boys entertained while running in the forest or driving long distances.
At the age of 11, Jung received a very special Christmas gift from his father: a book for teaching children the programming language C. Back then, Jung was already an avid gamer, but he was only granted a strict six hours a week on his PC. Soon enough, he had devoured that C book plus several more, and his parents doubled his screen time allowance so he could spend as much time programming as playing video games. Even before finishing high school, Jung knew that he wanted to become a computer scientist. That’s how he ended up enrolling at Saarland University, which was and still is a powerhouse in the subject.
“Discovering that there’s such a deep connection between logic and programming was one of my life’s biggest moments.”Professor Ralf Jung
It was there, in that fateful undergrad class with Professor Smolka, that Jung first learned about the proof assistant Coq, a tool for carrying out machine-checked proofs which has been instrumental in his research ever since. Jung describes his first encounter with Coq in Smolka’s class as “incredibly fun”. “Completing a proof in Coq would never fail to give me a shot of endorphin comparable to that of reaching the next level in a video game,” he recalls.
A stroke of luck leads to a job offer
When the time came to choose a topic for his Bachelor’s thesis, Jung had only one constraint: it had to involve doing proofs in Coq. That was also the one constraint that guided him when choosing the topic of his doctoral thesis. However, finding a doctoral advisor wasn’t an entirely linear process, nor was it governed by pure reason. Chance also played a role. One day in 2013, Jung came across a poster advertising research on machine-checked proofs. He emailed Professor Derek Dreyer, who was named on the poster, and within days got a response from him. It was a stroke of luck.
Professor Dreyer’s office was on campus but Jung knew nothing about him, since he was affiliated with the Max Planck Institute for Software Systems (and not directly with the university) and didn’t teach any courses (yet). “At first, I was hesitant about committing to my thesis topic, but Derek got me hooked by feeding me a steady stream of interesting little problems until one day he gave me the key to an office and asked me: ‘Should I pay you a salary?,’” Jung remembers. Dreyer continued to provide excellent support during the rest of the doctorate and even to this day. “He really is my “Doktorvater” in the best possible sense of that term, and I am deeply grateful for that,” says Jung.
Jung eventually completed his doctorate under Professor Dreyer’s supervision in the summer of 2020. In the nearly 300 pages of his dissertation, the Coq proof assistant – perhaps unsurprisingly – is mentioned 65 times.
Jung’s dissertation won several prestigious awards, helping to raise his profile as a leading researcher in the field of programming languages. At the same time, his thesis put him on the map as one of the top experts in the programming language Rust.
A programming language for secure software
Graydon Hoare started designing Rust around 2009 while he was a software developer with Mozilla. Jung got interested in the new language in early 2015, only months before the first stable version of Rust was released. Now, nearly 3 million programmers worldwide code in Rust, many of whom simply love the language, and tech giants of the calibre of Amazon, Google and Microsoft are increasingly building software using Rust. Even the White House has recommended that organisations start making more use of Rust in their projects as a way to make software more failproof and less vulnerable to cyberattacks.
The growing community that builds with Rust brings together thousands of enthusiasts, and Jung is proud to be one of them. Jung is convinced that many other people deserve more credit than himself for making Rust a success. But he undeniably played a critical role in creating the theoretical foundations to back up the claims of reliability and safety that have made it so popular and widely adopted by industry.
Indeed, much of Rust’s appeal stems from its designers’ promises about the performance and reliability of programs written in the language. They claim that code written in Rust will not only run very fast and give developers fine-grained control over what happens at runtime with critical resources like memory; but, by its very design, code written in Rust will also be free of some of the most common bugs that ail programs written in legacy systems programming languages such as C and C++. Rust achieves this by making sure that a wide range of errors that can occur in a program’s handling of memory are detected before runtime by the compiler – the software that translates the source code written by the developer into the binary code computers can understand. That way, developers don’t need to bear the burden of checking for those mistakes.
If their code is faulty, the compiler will return an error message with precise instructions on how to fix the issue. But the language also enables programmers to write code outside of this “safe mode”. The key to making “unsafe Rust” comply with the promise that the language is safe overall is to wrap the unruly pieces of code into libraries that, to the outside world, behave as if everything were written in safe Rust.
Using “Lego bricks” for mathematical proofs
In his dissertation, Jung proved that those libraries do indeed guarantee the safety promised by Rust’s designers. And to that end, he built a tool called RustBelt which researchers can use to perform formal proofs. “With RustBelt, we can prove properties of the Rust language that couldn’t be verified with the same level of confidence through software testing,” says Jung. RustBelt, in turn, builds on Iris, a framework that Jung codeveloped as part of his doctoral thesis. Iris provides a series of building blocks that make it easier for researchers to create mathematical models and conduct formal proofs on any programming language, not just Rust. With Iris, those researchers now have a set of reusable pieces that they can put together for whatever proofs they’re constructing. “It’s like having Lego bricks to make mathematical proofs on the computer, and people sometimes put together impressive towers,” says Jung.
Iris is what experts call a “concurrent separation logic”, a theory that allows researchers to analyse what happens in a program where more than one process accesses the same data simultaneously. That concurrency is crucial in modern programming, as it allows code to run faster on state-of-the-art multi-core processors. But concurrency is also the source of common errors that lead to programs crashing uncontrollably or being hacked into by cyber criminals. With Iris, researchers can prove that a concurrent program is reliable and secure, properties that are very hard to ensure through testing.
While RustBelt is designed to help us better understand Rust as a language, Stacked Borrows, the third contribution made by Jung’s doctoral thesis, aims to develop Rust further by enabling the compiler to optimize the code written by developers, making it more efficient in turn. Over the last few years, Jung has gone on to build more tools, all with the goals of creating as accurate a model as possible of how Rust’s key components behave and providing mathematical proofs to increase developers’ confidence in the language.
Jung foresees a promising future for Rust, with companies adopting it more and more for new projects in which performance, efficiency and safety matter. “Rust is one of the best shots we have at improving software, which is in a sorry state at the moment, unfortunately,” he says. Hopefully, it won’t be long until Jung’s dream of a world free from software bugs becomes reality.
Ralf Jung is an assistant professor at ETH Zürich, leading the Programming Language Foundations Lab, which is part of the Institute for Programming Languages and Systems. His research focuses on the programming language Rust and the Concurrent Separation Logic Framework Iris. Previously, he completed his doctoral degree at the Max Planck Institute for Software Systems and Saarland University in Saarbrücken, Germany. He also did a post-doc in the PDOS group at MIT CSAIL.