when relevant content is
added and updated.
In January I read a news report about the DeepSpec project that is being developed by a few universities through a NSF grant. The press release had some bold claims, specifically that this project might be the answer to many people’s dream of bug free software. I had as emotional reaction to that. Ever since software was a thing, people have been trying to make it bug free. But, no matter how detailed the specification is, or how much *DD the programmers use, or how good the testers are, there are bugs in prod. It’s just the way of the world.
Bug free software may not exist, but that doesn’t mean the DeepSpec research project isn’t interesting or potentially important. Princeton University in New Jersey announced a workshop on the project, so I put some skin in the game and went. Here is a little bit about what I found there.
The DeepSpec workshop spanned about 3 days (day three was shorter) and the material ranged from “I’m completely immersed and get this.” to “I have no clue what is going on, where am I”? The first day was mostly a warm up round. The project director, Andrew Appel, opened up by explaining the the project, how all the universities tie in together, and basic info about the workshop. There were a mixture of talks from industrial partners that were involved in the project, and university professors working on the project to specify specific versions of the C compiler or the Haskell programming language.
Day 2 felt heavier on the industrial partner side. There were talks from employees of Cisco, Google, and Intel talking about what life was like using formal verification methods on their projects. Most of these projects were very low. Google was attempting to use low level verification on a SSL project, and Intel and Cisco were using it for hardware design.
Day three was the part where I was completely out of my depth. This day was mostly code demos. The code for this project is written in Gallina. Think back to high school geometry, or maybe college calculus. Do you remember what a mathematical proof looks like? That is exactly what the Gallina code looks like and is. This isn’t your average software development tool and it isn’t like unit testing for any stretch of the imagination.
The DeepSpec project is focused on the lowest level parts of a project; think compilers, languages, kernles, operating systems, microprocessors, and the like. Each of these things has something in common. They come with very specific sets of rules. When people build these tools, there are specifications and the behavior is mostly understood. What’s that you say? All specifications are incomplete, or out of date, or just wrong? You are exactly right. And, even though most of the people present were students and university researchers, they understood this problem very well. One example from the heartbleed SSL bug went something like “If only that read condition were in the specification, that bug would have never happened”.
So, my initial, very allergic reaction to the DeepSpec press release was a little wrong and a little right. While I don’t think this type of effort will be viable for most commercial products, and I definitely don’t think there is such thing as a bug free product, I do think they are do something very important. We may not care whether or not the latest version of flappy birds matches up with the specification. Heck, there probably is no specification. And so goes a lot of modern development projects. But, for some areas — automotive, security, embedded healthcare systems, compilers — following a specification is very important. We have a pretty good idea of how a heart monitor should work, and are able to describe that pretty well. I’m looking forward to seeing how this project develops and whether or not it can get absorbed into the commercial software development world.
Side note: If you know about other research projects that vaguely fall into the testing, or verification realm, let me know. I found my happy place in Princeton and would love to go back.
More to come on this.