Dmytro Traytel

Project title

Discover: Distributed Streaming Computations, Verified

What is your project about?

Today's software and hardware systems produce massive amounts of data. Stream processing frameworks are vital tools for software engineers and data scientists to tame and use this data. They provide convenient programming abstractions that allow their users to express the desired data analysis. Mature stream processing frameworks like Apache Flink or Google Cloud Dataflow are huge pieces of traditionally developed software, but despite their success they have thousands of known correctness issues that endanger their availability or may cause data loss. DISCOVER proposes to develop a new efficient, expressive, and trustworthy stream processing framework. To provide the highest level of trustworthiness, we will use a proof assistant to design and implement the framework and to prove its correctness.

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

Proof assistants are wonderful software tools. They meticulously check human-written mathematical proofs and assist their users in constructing these proofs. They are used today to verify deep mathematical results and highly critical software, which cannot tolerate correctness errors. My first encounter with the popular Isabelle proof assistant happened during my B.Sc. studies at TU München. I became "addicted" soon thereafter and am an Isabelle developer and an Isabelle user today. Often these activities are carried out by different researchers, but they are highly symbiotic: Being a user lets me find out how well proof assistants work and get inspiration for new features. And understanding how the proof assistant works under the hood helps me use it effectively.

What are the scientific challenges and perspectives in your project?

Developing distributed streaming algorithms that can run in data centers for improved scalability is challenging. Proving that such algorithms do what they are supposed to do even more so. And having to convince a proof assistant of your proof's validity certainly does not simplify the task. But there is hope: stream processing frameworks enforce a program structure that is susceptible to a high degree of parallelism. Thus, algorithms expressed using such frameworks can be distributed naturally, while the programmer mostly has the illusion of working with a non-distributed computation. DISCOVER's main research hypothesis is that the same applies to the correctness proofs: proofs for a non-distributed computation can be lifted to the distributed setting.

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

DISCOVER will produce the first formally verified system for the reliable analysis of big data. The strong correctness guarantees will make it possible to use the developed stream processing framework in safety- or mission-critical scenarios, which cannot tolerate incorrect data analysis results. Moreover, DISCOVER has the ambition to make it easy for its users to prove the correctness of applications developed using the framework. The project will thus provide the necessary firm foundations for the work of software engineers and data scientists and thereby contribute to the wider adoption of proof assistant technology.

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

The generous Sapere Aude: DFF Starting Grant will in the short term allow me to focus on an ambitious, open-ended research question, rather than picking lower-hanging fruits. In the long term, the Sapere Aude grant will help me to consolidate my position as a research leader in interactive theorem proving, the science of proof assistants. With this project, I am also entering a new research area, data stream processing, which I have so far encountered in my research only from a user's perspective. My ambition for DISCOVER is to change the way one thinks about correctness in this research area, similar to the profound impact the first formally verified operating system, seL4, had on operating systems research.

Background and personal life

I was born in Kharkiv, Ukraine and grew up, studied and did my PhD in Munich, Germany. After a five year stint as a postdoctoral researcher in Zurich, Switzerland I moved to Copenhagen, just in between of two Covid waves. When I am not hunting for the next "qed" with Isabelle, I enjoy cycling and playing board games. On the weekends, I can frequently be encountered together with my son and wife in the Bastard Café, our favorite spot in Copenhagen.