[FOM] Object-Oriented Formal Mathematical Languages

[Brian Postow]

Victor Makarov spake:

> such as, for example, integer numbers). So we may say that a class is to an 
> object (of the class) as a mathematical theory is to a model of the theory 

Another way of looking at it is to say that a class is the type of an
object. If we use the Curry-Howard Isomorphism, we can translate that
class into a logical statement, and that object into a proof of that
statement. 

Now, I'm not sure what logical language would be used for that,
perhaps that's really the original question. I haven't seen
Curry-Howard translated into object oriented languages, but I would be
very interested in what it looks like in that environment. 

Also, I should note that most of the models I mentioned earlier are
object based rather than class based, mainly because it's a lot easier
to model objects than to model classes. (although both Abadi and
Cardelli, and Castagna model classes in their respective books)

Brian Postow