Is Code Verification Finally Good Enough?

Jonathan asks: "As someone who has been following the development of software verification technology, a recent trend has intrigued me. It seems that the formal method people have finally come down off their high horse and are offering code verification as just another tool. This approach shows up in recent Java and C# based code verification tools that aren't aimed at 'proving correctness' so much as finding potential errors. Now it seems that such an approach is beginning to find its way into XP methods[pdf] as another verification tool to supplement unit tests. Given the current speed and effectiveness of tools like the Spec# verifier, is code verification via automated theorem proving finally going to make its way into the mainstream?"

Comments

No :)

[Monkelectric]

The thing you have to remember about methodologies is they are all bullshit. In my experience, the people who cling to methodologies are generally not clue-full.

The paper you linked to -- I just finished reading it. The "methodology" they provide has more comedic value than anything else. The steps in his methodology are counter-intuitive and therefore stupid. He wants us to iterate over each requirement, re-writing a function as the most simple program which passes the tests? What possible reason for this would we have other than an exercise in futility? Writing code we *KNOW* has no value with the intent of re-writing it later? Futile.

Perhaps you could accept this premise if the methodology scaled for larger problems -- but clearly it does not and can not. At this point I suspect you are the author of this paper.