I began reading chapter 3 on program proofs last night. Once again I was struck by the length of the proof for a simple program -- two pages or so for a 10-liner! This is clearly not scalable. The effort (not to mention paper) required to prove a real-world project would dwarf that required to write it in the first place. Small wonder that gcc, Oracle, the Solaris kernel, Adobe CS4, Apache or Asterix (just to name a few large-scale, real-world projects) do not come with proofs, as far as I know. Were anyone to begin to work on proofs for even a small subsystem of these, they'd be up for retirement long before they could finish.
The method given for program proofs also seems to omit critical aspects -- side effects. It is fine to show that a program produces the required output when given proper inputs, but if it leaks memory or stomps on memory it doesn't own or opens holes that can be exploited to break security, or calls routines that require cleanup but doesn't call the cleanup routines, etc., the "proof" is positively pyrrhic.
The author claims that some software organizations require a declaration of loop invariants, if not complete proofs. Maybe I'm from Missouri, but I need names so that I can follow up and confirm it. None of the software organizations I have worked in have ever required anything like that. My experience has shown me that software projects have tight schedules and even tighter budgets. Code needs to be commented, to be sure, and tested (usually by a separate team), but proven? Hardly!
Finally, a rhetorical question: How would you prove a program when the ultimate test of correctness is that the customer is satisfied it does what he wants? For example (a simple one. It's not hard to come up with a gazillion others), say you want to add a red-eye reducer to your photo program. How do you know it works? You only know that if the user is satisfied with the results. Oh, maybe you can prove that your program does the "right" thing in terms of what it does, pixel by pixel, but if the user still thinks it's garbage, your proof is worthless, both to you and your user.
Subscribe to:
Post Comments (Atom)
1 comment:
Prof. Hehner works on this sort of thing, including the idea of programming languages that are their own proof. Scaling is certainly a problem.
Let's scale this back down. Even lots of C code includes asserts --- far from complete proofs, but tests that the state of the program matches some invariant. These are "proven" by the program continuing to run.
The test-against-the customer problem is slightly different. I think we can only measure correctness against specifications, and what you're pointing out is that these are moving goalposts.
Post a Comment