>> The Eiffel guy had a chapter implementing a stack and "proving" that 
>> it matches the spec. 
> 
> That's actually impossible to do, since Eiffel isn't a formal language. 
> There's no definition for what "X = Y" means in the language (as in 
> assignment operator) so he can't mathematically prove it matches the spec.

The Eiffel assignment operator is actually ":=", with "=" representing 
(value) equality. But hey, I wouldn't know a "formal lanuage" if it hit 
me...

>> I think he was trying to counter the old "there is no mathematical 
>> theory to OOP".
> 
> And for the most part there isn't. There's hand-waving mathematics, but 
> not something precise enough you can automate it.

It's more the point that every OOP language has a slightly different 
idea about the precise definition of "object", "class", "inheritance", 
and so forth. (Some have SI, some have MI, some have class methods, some 
don't, some have private methods, some don't, some allow public 
attributes, some don't...)

>> At the time, I believed him. Having seen Haskell, and its evil twin 
>> the Lambda Calculus, I now understand what they mean by "no theory of 
>> OOP"...!
> 
> Yep, exactly. ADTs are the sorts of high-level data types you build out 
> of lambda-calculus type rewrite rules. LOTOS is the only actual 
> programming language I know of that goes all the way down to that level 
> of mathematical detail.

Even Haskell doesn't actually possess a denotational semantics - what 
ever the hell *that* means!

-- 
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*

Post a reply to this message