I am weighting my options on future research directions.
I have a long-term interest in formal methods in software engineering. In the past few years, I was especially interested in making these decoupled from the chosen programming language; that was also the gluing aspect of the work I was doing during my PhD studies. These days, as a postdoc at Newcastle univerity, I am working on methods for verification of programs that combine two programming languages: Rust and C. While these are fairly specific languages, I am trying to use the language-parametric techniques, this time not as an object of study but as pragmatic tools that help me be more economic.
Then, a question arises: what do I want to work on longer-term, after my postdoc days are over? Ideally, it would be something that (1) I can realistically do, while (2) enjoying it and (3) being of an use to the broader society. And since I can’t afford to run any research efforts on my own funds, the last property should be reformulated more as (3’) it is understandable to the senior members of the research community that the goal/plan/vision would benefit the broader society.
I am unsure whether (3’) is true about the language-parametric software verification project.
Successes and Failures of language-parametric stuff
I do not know when exactly was the “generate language tools from langauge definitions” idea born, but it is present already in the 2010 K-Maude paper by Traian Serbanuta and Grigore Rosu. The paper described an early version of the K-framework, based on the Maude rewriting system. Since then, the group of people around Grigore Rosu authored tens of related papers, and a company began developing the K-framework.
On the other hand, the ideas about language-parametric tools didn’t seem to make their way to researchers outside Grigore Rosu’s group. I will try to speculate about the “why?“s in the following paragraphs; however, the main point I want to make is: if the group of Grigore Rosu could not make their ideas to be accepted by the wider scientific community, despite all their scientific publications and some commercial success, then what would make me succeed in the same goal? Wouldn’t choosing such a research direction be too risky?
Some mistakes to avoid
Perhaps I could learn from the mistakes of the K-framework community and try to avoid them.
Rewriting, again
K-framework was originally a framework/library for Maude. Eventually, it got rewritten to Java, got an OCaml-backend for generating faster concrete interpreters, then it was rewritten around the (in)formal intermediate language Kore and got new backends written in Haskell and C++. During the development, the input language of K-framework changed multiple times, breaking the compatability with the existing language definitions out there. From personal communications with researchers outside the Grigore Rosu’s group I learned that such changes were percieved negatively.
Kore
At the point K-framework was rewritten to use the intermediate language Kore, it became too informal for precise reasoning required for scientific work.
Not interesting for “foundationalists”
There are groups of people that like doing machine-checked proofs. One such community is formed aroud the Iris separation logic framework. I guess that the informal nature of the implementation of K-framework makes K unattractive to groups like that.
Not interesting to practictioners, either
It appeared to me that the re-writing of K was partly due to poor performance of concrete interpreters generated by older versions of K (K-Maude?). Faster tooling is necessary to attract practically-minded people; however, recent K is still not fast enough - especially when one wants to use proof object generation to ensure correctness (1, 2). Informally, it has been conjectured many times that a partial evaluation of a language definition with respect to a program could be used to speed up all the language-parametric tools; however, I am not aware of any serious and published work using that technique.
The matching logic black hole
K and related theories make use of first-order pattern matching - the correspondence between terms with and without variables. In the early papers around K, this was made explicit by means of “matching logic” - an extension of first-order logic. However, since then, the name “matching logic” was used for (related but) different logics, which added some confusion. These different logics then became research projects on their own, consuming resources but ultimately not contributing to the vision of language-parametric infrastructure. I have also worked on matching logic, and while I have learned something during the way, now I think that I could have invested the time more productively.
Stuck with Hoare
Since Hoare’s 1969 paper until roughly the end of the century, reasoning about pointer-manipulating programs was a challenge. Separation logics (and related, alternative approaches) simplify pointer reasoning, and these days, there is a large community using separation logic for program verification. K could have been more appealing to these communities if it offered tools for reasoning in the separation logic style, instead of simple Hoare logic style (realized as Reachability logic).
Some things that worked
Accessibility of K
I was able to use K as a master’s student, without any knowledge of theorem provers. The frontend language is easy to learn and relatively expressive.
Selling results, not techniques
In 2015, there was a PLDI paper about semantics of JavaScript in K. But perhaps it was not the semantics itself that sold the paper, but bugs in browsers that the authors discovered? Similarly for the formalization of undefined behavior in C.
So, what other options for a longer-term research vision are there for me?
Language evolution without the pain
I conjecture that techniques based on programming language semantics can help the society address the problem of programming language evolution. These days, evolution of programming language is painful. I am aware of five options currently used for that purpose: (1) do not do any significant evolution (C), (2) evolve and keep backwards compatibility (C++), (3) evolve and ignore backwards compatibility (Python 2/3), (4) evolve and tie programs to particular compiler versions (Rust, Haskell), (5) evolve and provide upgrading tools for migrating source codes that use older version.
All of these options have their drawbacks. As for (1), this approach ignores all the progress that happens in the area of programming languages, and we have already been there for way too long. As for (2), everyone knows how complicated C++ got over time, to the point when nobody understand the language specification. As for (3), it is also a common knowledge that transitioning from Python 2 to Python 3 was a pain. Regarding (4), besides the easy-to-be-made mistake of confusing language versions with compiler versions, this only solves the issue of an automatic upgrade breaking the resulting binary, but it does not help the programmers use new language features. The option (5) is the one I would prefer, but writing such upgrading tools manually is a lot of work and error-prone. Perhaps we could synthesize these automatically, utilizing the knowledge of the old and new language definitions?
The first step in such a research program could be to create a dataset with pairs of language definitions, each pair representing a feature change inspired by a change that happened in a real-world language.
Conclusion
So what is next? I am not sure; all these are more thoughts about the future possibilities rather than plans to immediate action.