Verified code is something which has existed in the research labs of computer science departments for decades now. You may remember it as one of the goals which drove the initial development of functional languages: the dream that we could make a claim about the way a software system will behave, and then verify that it’ll always hold true. Properties about software like that it won’t crash, that it won’t fall into an infinite loop, and that it won’t divulge classified information to the Chinese no matter the input or the circumstance.

That’s all nice and good, but why is such a thing important? Well, I’ve seen it estimated that there are as many as 5 bugs per every hundred lines of code. The more code you have, the more bugs are likely to be present. Version 2.6.0 of the Linux kernel weighed in at just under 6 million lines of code. That is, by this estimate, roughly 300,000 bugs. It is unlikely that you could write something that does as much as the Linux kernel and be significantly smaller in code size to boot.

BUT, with verified code there can only be as many bugs as there are in the description which was fed to the code verifier. And descriptions are often much, much smaller than the code they describe. For a full-blown UNIX-like system, like Linux, this may be on the order of around 10,000 lines of “code.” By the same metric, that equates to only about 500 bugs! That’s a heck of an improvement. (these numbers are made up, the phenomenon I’m describing is not). For an ideal, next-generation secure operating system that doesn’t have to worry about compatibility, I would wager that this could be on the order of only a thousand lines of code. I’m sure it could even be brought down to a few hundred lines of code if that were an explicit goal. That’s a total of 5 to 50 bugs in the entire system, for those of you who are counting.

That’s not a big deal; it’s a huge deal.

So why isn’t code verification commonplace today? Well because of something called the computability problem, you can’t just slap a code verifier on top existing software and expect it to work. Software has to be redesigned from the ground up with code verification in mind in order to get any use from it. And that’s just too much work to ever see happen, right? Well, not really. We’ve done it once; remember GNU and Linux? The problem back in the 80’s and 90’s was proprietary software and compatibility, and for that we needed open source software. Now the problem is security and reliability. And for that we need verified code.

There are a few out there who understand the issue. Microsoft Research’s Singularity operating system uses verified code at every level of the system possible. This gives me hope. But for something like this to make it out of the research labs and into mainstream use will require a lot of work. We’ve seen how open source can make even the largest of projects seem simple… perhaps the time has come to refocus our efforts?

Well, don’t make me do all the work myself.