HELP! formalizing OO
Alan C. Kay
alank at wdi.disney.com
Sat Apr 25 03:54:42 UTC 1998
Computer stuff already is mathematics, but of a new kind. Trying to reduce computing to classical math is generally a mistake. If you think about math in terms of "p implies q" (which was Russell's definition of math) instead of something derived from set theory, then a whole working OOP system that is spun out of a few primitives is as least as impressive as Euclid's Elements or an Abstract Algebra (in fact it is a new kind of Abstract Algebra). Another interesting point here is that classical math is a kind of clockwork where everything has to mesh and a single error should stop the clock -- computer math is more like biology where we want to successfully make more complex things out of less complex things, but we don't want most errors to be able to break things, instead, we want the new math to accomplish its "proofs" in spite of possible "broken gears".
In other words, what could be more formal than a computer program that a computer can actually run? Remember that lots of classical proofs had serious errors that no one noticed for a long time. Heavy formalization didn't really help all that much ...
At 12:31 AM -0400 4/25/98, Florin Mateoc wrote:
>Could someone please point me to existing research in formalizing the OO
>approach (in relationship with fundamentals of Mathematics, Set Theory)?
More information about the Squeak-dev