Friday, August 15, 2008

Using Theoretical Proofs to "prove" Program Correctnesss

I read an article the other day called "Goodbye to Faulty Software." The article had one of those catchy titles that I saw while I was catching up on ACM Technews. The title itself intrigued me because faults in software (or, defects) are something that I tend to deal with on a regular basis. The author(s) of the article talk about writing a proof using the language of logic that will ensure that software does what it is supposed to do.

I began to dig into the content that the article referred to and found a bunch of open source tools that help you specify a logical proof that can then be generated into a program. I would be telling falsehoods if I even insinuated that I understand both the theoretical foundation or the contents of the tool documentation at this point, as I have only begun to look it over, but there are some questions that come to my mind. For example, how can the proof be proven to be true unless the developer and the customer are able to speak the same language? Or, have I missed something extremely basic whereby the languages used are merely a manifestation of some specification that is (somehow) reduced to its mathematical form? In either case, I am intimating one thing that seems to make sense to me: If the customer(s) and the developer(s) can speak (or write, or formulate, etc.) the same language and it can be guaranteed that the language will produce the results that the customer is looking for, I think it would be a step in the right direction. Of course, if it gets good enough, would we need a programming staff to implement this stuff? (I know we would, but it is an interesting question to let my mind play with).

I am hoping I can get someone (or some paper) to give me the reader's digest version of this whole topic so that I can at least grasp the entire concept before wading into the details, but that may not be possible. The topic itself seems to be complex and it goes into areas of mathematics that I have not used for some time. So, we shall see. Telling will be what I write my next blog entry about.