As my PhD defence is approaching, I am reflecting on why I got into that research area - the area of formal methods for software engineering. Unlike for many of my research peers, it was not an innate interest in theory or mathematics that got me there; rather, my motivation was practical. The journey began when I got my first software engineering job (back in 2013), and was started by a question: “How can I write software better?”. The tentative answer was, and still is: “By having better tools”.
My first programming job
Since the summer of 2013 until the fall of 2017, I was working part-time at an embedded systems company, writing firmware for the company’s in-house made devices. It was an invaluable experience: the atmosphere was good, the tasks interesting, and what I was learning was complementary to my university studies. I felt good, but sometimes, a bug slipped under my hands.
It seemed to be happening to everyone. Our code was not that buggy - most of the time, things worked reasonably well. But still, bugs were affecting our life more than I liked. Even the C and C++ compilers that we used sometimes crashed on some trickier-but-technically-valid code. We are not as good programmers as we should be, I thought now and then.
At some point, I started paying closer attention to compiler diagnostics, since they were often helpful when troubleshooting why my code does not work. At some point, when the codebase compiled without compiler warnings, I started exploring various static code analysis tools. I also learned I was asking the wrong kind of questions.
The question of two “Why?“s
Asking the question “Why my code does not work?” usually led me to debugging sessions where I was spending time stepping through my program, looking for the point where things go wrong. But pointing to the step where things go wrong is hard without knowing the intended code invariant – that is, without knowing what is the thing about the program that stays the same as the program progresses.
So instead, I started asking: “Why this code should work?”. That led me to (1) specifying what I want the code to do, and (2) thinking about arguments for the code correctness. Fortunately, there were tools like Frama-C that allowed me to express such a deductive argument in terms of contracts and invariants; Frama-C would let me know if my argument was wrong. Unfortunately, Frama-C worked only with C code; I was writing C++ and could not find any deductive verification tool supporting C++.
A quest for better C++ tools
Around 2016, during my search for better (or, at least, some) tools for reasoning about C++ code, I discovered K-framework: a tool for building programming language tools. I contacted the main brain behind the framework - Grigore Rosu, a professor from Urbana-Champaign - saying that I would like to work on C++ support in K-framework. We exchanged a few emails, resulting in me starting the work on what later became my Master’s thesis.
The thesis was a success. Sadly, the project of building a tool that would let me know if my argument about C++ code is wrong was not. There were multiple reasons for the failure; these are beyond the scope of this post. After the thesis, I started doing a PhD in this area of formal reasoning about software, and it was fun.
Conclusion
The projects I was working on during my PhD studies may be seen as too theoretical by many people. In my own eyes, they were was motivated by the question: “Can we have better programming language tools than what we have now?”. I want to keep that in mind while preparing for my defence.