Though it's infeasible to prove a program correct, how about proving things like "consistent" or "safe"? Even if it's too hard to prove that a robot arm will build a car, it would seem reasonable to prove things like, the arm doesn't start drilling holes in itself or in nearby workers.
To an extent this is already done via type-checking of various sorts. But type-safety is a pretty weak constraint.
Such things wouldn't give you a proof of correctness in a traditional sense, but they would you help convince *yourself* that a program is likely to work properly.
Lex
Jarvis, Robert P. writes:
I think this is an interesting topic. Being able to come up with a proof of a given programs correctness would be wonderful, but I think this is often impractical in the "real world". To be able to prove that a program will behave correctly you have to define what the correct behaviors are, and in many cases the definition of "correct behavior" is a moving target. So you may be able to prove that a program meets a set of specifications which existed at some time, but can you then prove that the specifications are correct? The chicken and the egg trade places, the wyrm devours its tail, and we iterate again. :-) There's also an analogy here to solving some production optimization problems which are at once too complex and too loosely defined for solution by traditional methods. What you find is that although you may not be able to determine the "optimal" solution, a "near-optimal" solution is good enough and requires a fraction of the computation time. In software I think that providing an environment where correctness is probable, if not provable, is probably the "near enough" solution.
Bob Jarvis The Timken Company
-----Original Message----- From: Steve Dekorte [SMTP:steve@inquisit.com] Sent: Monday, April 27, 1998 8:39 PM To: squeak@cs.uiuc.edu; dnelson@redwoodsoft.com; David-Joerg@deshaw.com Cc: The recipient's address is unknown. Subject: Re: HELP! formalizing OO
Florin wrote:
..I would say though that math looks to me like it is still ticking,
An interesting thing about math/logic is that it can prove some of it's own limitations.
I think I remember hearing about proofs of the insolvability of the n>2 body problem and of general solutions to finding the roots of polynomials above a certain order.
If these problems are provably insolvablable, should we have much confidence in what seem to be the more complex problems of large programs being solvable? (By solvable I mean knowing everything about what they do without actually running them)
I think most everyone sees that complex programs (like n>2-body problems) can't be analyzed without computation, so there are two choices.
The top-down approach is to attempt to make programming langagues more analyzable before computation (Strong typing, etc) so correctness can be proven. This approach is basically out to eliminate the dynamic aspects of the system that lead to complexity. (Of course if Smalltalk can be written in ADA, how is ADA more provably correct or "safe"?)
The bottom-up approach is to look for new ways of managing complexity so correctness is more probable. OO of the Smalltalk type is, IMO, an example of the 2nd approach. It looks at real the source of chaos - excessively coupled equations (via variables) and structures the langauge to make this problem easier to avoid.
So while the top-down thinkers are unsuccessfully trying to make correctness provable, the bottom-up thinkers are successfully making correctness more probable.
Steve
Though it's infeasible to prove a program correct, how about proving things like "consistent" or "safe"? Even if it's too hard to prove that a robot arm will build a car, it would seem reasonable to prove things like, the arm doesn't start drilling holes in itself or in nearby workers.
To an extent this is already done via type-checking of various sorts. But type-safety is a pretty weak constraint.
More practical than proofs is the ability to *reason*. Object oriented programs improve the ability to reason about more complex systems. You may not be able to *prove* that a robot would not do this or that. But you can *reason* that this woud not be so.
OTOH type checking is itself a proof, so to the extent you can extend types into areas like "drilling with robot arms" you can begin to prove things about those things. This is what the Haskell language does with monads. It can prove things like I/O operations, if they are performed at all, will be performed in the order specified.
squeak-dev@lists.squeakfoundation.org