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.

-- 
Patrick Logan                 mailto:patrickl at gemstone.com
Voice 503-533-3365            Fax   503-629-8556
Gemstone Systems, Inc         http://www.gemstone.com