At POPL someone asked after some verification talk what was different about this current wave of hype regarding machine-checked proofs of correctness. The speaker discussed how we have developed better proof techniques and our machines have gotten a heck of a lot faster, so maybe this time verification is here to stay. I have been thinking a lot about the question of whether verification is here to stay and why. While I buy the "machines are faster argument," I still think a lot about the role of verification in our daily lives.
Something interesting to think about is the proofs as social processes paper which supposedly killed verification for a bunch of years. This paper says that because proofs are not meant to be completely formal and only meant to be discussed among mathematicians, machine checked proofs are not going to do anything for us. While de Millo makes a good point that verification still doesn't tell us about some absolute notion of correctness, his tone is very extreme and there seem to be many red herrings. (For instance, he uses Rabin's pseudoprimes as an analogy for the concept that we should regard mathematical proofs as "probably correct.") Also, one of the main points seem to be that verification will not go anywhere because the proofs are too long and ugly he doesn't address the counterargument that maybe mathematicians have been doing it the other way because machine proof techniques were not good enough.
This paper generated some interesting discussion at the last Software Design Group tea, which I sometimes crash. There were extremes of opinion: while some people thought the paper was well-crafted and prescient, there were others who were so angry with the argument and the manner in which it was made they were ready to physically defend their principles. At this tea I learned that the de Millo paper was targetting the views of those like Dijkstra, who believed in a notion of ultimate correctness. Dijkstra wrote a colorful rebuttal comparing the de Millo paper to a "political pamphlet from the Middle Ages"--also a good read. ;)
2 comments:
It is hard to say whether verification is here for the long run, or whether it has even yet arrived. Obviously it is once again making significant inroads into POPL and other PL conferences, but the mention of "program verification" in the context of proofs and theorems usually emits a blank stare among my undergraduate CS friends and friends in industry.
I'm inclined to take a middle stance- there is a lot of interesting work to be done in advancing the state of the art in [insert favorite proof assistant], and I think such tools will be more readily used in the production of proofs for papers. As a reader of papers, it is much more assuring to me that proofs have been well-thought out if they have been subjected to the rigors (read: mundane details) via a proof assistant. Properly formatting arguments for input to a restricted theorem solver may also have additional benefits (better turn around, standardization of proofs, and others) but I don't have enough experience to know.
In the opposite corner, developers of software in the mainstream are very unlikely to use or desire any sort of the verification performed by Coq/Isabelle/.. as it is usually not pertinent to working "well enough" and meeting deadlines. Perhaps it is one more level in the tradeoff between development effort and program correctness/safety (the current one being the decision of static or dynamically typed languages).
The sort of verification offered by proof assistants is certainly useful to those requiring proofs- my greater question is whether the market for proofs, whether of type soundness or of program correctness, can be expanded beyond writers of type systems and those requiring extremely reliable (provably correct) software.
I support the verification but when it takes so long time and then we have to wait for unnecessary cause it makes us so unhappy. So we need to be more awareness about this and we can work to change the old system.
Post a Comment