HELP! formalizing OO
lex at cc.gatech.edu
Tue Apr 28 16:40:27 UTC 1998
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
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.
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 at inquisit.com]
> >Sent: Monday, April 27, 1998 8:39 PM
> >To: squeak at cs.uiuc.edu; dnelson at redwoodsoft.com; David-Joerg at 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
> >and of general solutions to finding the roots of polynomials above a certain
> >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
> >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
> >is more probable. OO of the Smalltalk type is, IMO, an example of the 2nd
> >It looks at real the source of chaos - excessively coupled equations (via
> >and structures the langauge to make this problem easier to avoid.
> >So while the top-down thinkers are unsuccessfully trying to make correctness
> >the bottom-up thinkers are successfully making correctness more probable.
More information about the Squeak-dev