Open Proofs: New site and why we need them
There’s a new website in town: http://www.openproofs.org. This site exists to define the term “open proofs” and encourage their development. What are open proofs, you ask? Well, let’s back up a little…
The world needs secure, accurate, and reliable software - but most software isn’t. Testing can find some problems, but testing by itself is inadequate. In fact, it’s completely impractical to fully test real programs. For example, completely testing a trivial program that only add three 64-bit numbers, using a trillion superfast computers, would take about 49,700,000,000,000,000,000,000,000,000 years! Real programs, of course, are far more complex.
There is actually an old, well-known approach that can give much more confidence that some software will do what it’s supposed to do. These are often called “formal methods”, which apply mathematical proof techniques to software. These approaches can produce verified software, where you can prove (given certain assumptions) that the software will (or won’t) do something. There’s been progress made over the last several decades, but they’re not widely used, even where it might make sense to use them. If there’s a need, and a technology, why hasn’t it matured faster and become more common?
There are many reasons, but I believe that one key problem is that there are relatively few fully-public examples of verified software. Instead, verified software is often highly classified, sensitive, and/or proprietary. Many of the other reasons are actually perpetuated by this. Existing formal methods tools need more maturing, true, but it’s rediculously hard for tool developers to mature the tools when few people can show or share meaningful examples. Similarly, software developers who have never used them do not believe such approaches can be used in “real software development” (since there are few examples) and/or can’t figure out how to apply them. In addition, they don’t have existing verified software that they can build on or modify to fit their needs. Teachers have difficulty explaining them, and students have difficulty learning from them. All of this ends up being self-perpetuating.
I believe one way to help the logjam is to encourage the development of “open proofs”. An “open proof” is software or a system where all of the following are free-libre / open source software (FLOSS):
Open proofs do not solve every possible problem, of course. I don’t expect formal methods techologies to become instantly trivial to use just because a few open proofs show up. And formal methods are always subject to limitations, e.g.: (1) the formal specification might be wrong or incomplete for its purpose; (2) the tools might be incorrect; (3) one or more assumptions might be wrong. But they would still be a big improvement from where we are today. Many formal method approaches have historically not scaled up to larger programs, but open proofs may help counter that by enabling tool developers to work with others. In any case, I believe it’s worth trying.
So please take a look at: http://www.openproofs.org. For example, for open proofs to be easily created and maintained, we need for FLOSS formal methods tools to be packaged up for common systems so they can be easily installed and used; the web site has a page on the packaging status of various FLOSS tools. Please feel welcome to join us.
path: /oss | Current Weblog | permanent link to this entry