Where is the economic argument in program verification research, and where are the salvation messages in software engineering research?
I just had the pleasure of attending David Rosenblum’s keynote at ASE 2016, in which he praised the power of probabilistic thinking (using stochastic reasoning to estimate risks and support decisions) versus an absolutistic view in which there is only 100% truth or 100% failure. His takeaway message was that software engineers should embrace probabilistic methods and permeate them throughout the development process.
As a software engineer, probabilistic thinking is a central part of my day-to-day job – in development as in research. Whatever I build and design, I think about how useful it might be, which benefits it may bring, and what the associated risks are. In Software Engineering research, the dominating metric is usefulness, which eventually translates into an economic argument: What does it cost? What are the benefits? What are the risks? These are day-to-day questions in software development, and my research is expected to provide facts to help answer them.
In other fields of computer science, such as software verification, the economic perspective is much less argued about. Instead, the message touted is an absolutistic message of salvation: If you apply this technique, you will get a 100% guarantee that your software satisfies certain requirements – that the computation will be correct, that it will not crash, or that it will terminate within specific time bounds. For developers and society, this message feels like the second coming of Christ: The day will come and all your problems will be gone.
Up to now, there are great examples of how software verification works, and there are impressive examples of it being successfully used in practice; and just to be clear: By no means would I want to reduce these research efforts. But the systems formal verification is applied to are still small and constrained; and getting it to scale and widen will require enormous human effort reshaping existing systems – before salvation comes repent. Do we actually know how costly formally verified software is? Do we know how to teach its techniques to developers who do not hold a PhD? Can we estimate the risks it brings to rely on freshly written specifications, rather than on mature systems? Might "good enough" software be good enough? When talking to researchers in software verification, such economic arguments are frequently missing in the debate. But as a society, we need to understand where money is best spent, and answers to such questions could very well guide the field of software research.
Conversely, just as formal verification may benefit from introducing an economic perspective, Software Engineering may profit from adapting a stronger salvation perspective. What is it that Software Engineering research could produce that would be seen as a salvation in software development – a significant reduction of costs or risks? Recent topics that come to my mind are automatic software debugging and repair, steering development processes based on mining software histories, or massive automated test generation. Can we translate our capabilities into grand challenges that will provide salvation in the future, possibly even including guarantees? Yes, I know there are “no silver bullets” in software development. But any great research community should pursue great dreams as well as provide facts – and in this, all of us computer science researchers are in the same boat.
