Coming Up With The Wrong Formal Answer

It was a surreal moment. I was sitting in a conference room in Portland listening to a panel session about formal methods. The topic was discussing the fact that there is insufficient education at the undergraduate level in formal methods and algorithmic approaches to verification.

You can read about the panel here. In the question and answer session, a point was made that formal methods stop being called formal methods when they reach mainstream adoption. This was the very point I had made several years previous when people asked why formal technology never seemed to get anywhere. I gave them examples of where formal has been adopted — equivalence checking, clock domain crossing, X propagation… When it has solved an industry problem it acquires a name related to the problem it solves. What struck me sideways was when the same person who made the comment suggested that the way to fix this apparent failure of formal was to not allow people to stop calling it formal technology, but to celebrate the internal technology, the algorithms, that had made its solution possible.

How wrong can you interpret my original statement and what a wrong approach to the problem! The answer should have been simple. First nobody in the industry cares about the underlying technology used to solve a problem. They care that a solution exists, that it provides the necessary ROI to make the creation of industrial tools worthwhile and that those tools solve a problem for the industry in a better way than had been offered in the past. Does anyone care about the way a simulator works? No, they care that it makes their model run so that they can see how it behaves. Do they care which algorithm is powering their formal XYZ tool? No. I have never heard that colleges should be teaching people about how simulators work. It is irrelevant except to those who may be interested in implementing simulators.

Tools exist that utilize formal technology, and yet when those tools are released the last thing the creator wants to tout is the underlying technology that may drive part of the solution. The industry doesn’t care. They want the solution, they want it to do a job for them, they want a positive ROI from it. Everything else is irrelevant.

So, maybe I should be a lot more specific when I make statements and ensure that there is no way to misinterpret it. What should the formal community do about this problem? Spend more time working out how to apply the technology to solving problems that the industry has. Sure, there needs to be research into new and improved algorithms, but until they are used to solve an industry problem they are…well…totally academic, and nobody except the academic community will care about them.

See also:
Cracking the Tough Nut using Formal Methods
Do Students Need More Formal Education?