Re: "foundations built on sand"

I guess it is time for me to jump back into this discussion since my 
book (Foundations of Object-Oriented Languages: Types and Semantics) is 
again the focus of discussion.  I'll add my response after Thomas' comments.

Thomas Streicher wrote:
> This last example also brings to the point that one NEED not insist on 
> denotational methods, also operational or proof-theoretic methods definitely
> can do the job. Just sometimes denotational methods are more concise and, 
> therefore, much easier to grasp.
> This brings me back to my original question concerning translation of SOOL
> to META + F_{sub,rec,state}. From my point of view everything would be ok 
> if the target language  F_{sub,rec,state}  were endowed with an appropriate 
> operational semantics. I haven't seen such work and it is not contained in the
> FOOL book. Some of it is sketched there but operational semantics of state 
> isn't dealt with at all and that's what I consider most critical.
> As I understand the main theorem is that
>    (Sound) if  t : A  in SOOL then  [|t|] : [|A|]  in META
> this definitely should be accompanied by a proof that
>    (Refl)  if [|t|] doesn't give rise to a run time error 
>            then t doesn't give rise to a run time error
> This second property is rather assumed than proved. That's my impression 
> though I really might be mistaken as I didn't read everything in detail.
Unfortunately, this misses the entire point of a translational 
semantics.  The idea is that we compile SOOL to META and then run the 
translated program in META.  The reason you did not find the (Refl) 
property proved anywhere is that I did not provide a direct (run-time) 
semantics of SOOL!  Hence this property doesn't make sense in the 
context of my book.  However, see below.

> In any case I don't insist on denotational models though I definitely prefer
> them when available. Also operational methods may allow one to find 
> conceptually clear invariants (`a la logical relations) that allow one to 
> guarantee the absence of some undesired effects.

I have used a variety of different semantics in studying these languages 
over the last 10+ years.  Originally I used a denotational semantics for 
FOOPL, a functional OOL (see A Paradigmatic Object-Oriented Programming 
Language: Design, Static Typing and Semantics, Journal of Functional 
Programming 4(1994), pp. 127-206), but wasn't happy with the fact that I 
didn't know a model with all of the features I needed, and, besides, I 
was interested in moving to an imperative language where operational 
semantics seemed more appropriate.  Since then I have a couple of 
different operational semantics for imperative extensions of this 
language.  The most recent version (PolyTOIL: A type-safe polymorphic 
object-oriented language, by Kim B. Bruce, Adrian Fiech, Angela Schuett, 
and Robert van Gent) is about to appear in TOPLAS.  It can also be 
gotten through my web page at:

It uses a (natural -- big-step) operational semantics to prove 
type-safety via a subject-reduction theorem.  The development is long 
and technical, but does provide direct run-time semantics for a 
polymorphic object-oriented language very much like language PSOOL from 
my book (it essentially adds polymorphism to SOOL).

Perhaps if I had used that in my book, you would have been happier. 
While I personally believe I get a good intuition of the run-time 
behavior of OOL's from the operational semantics, for pedagogical 
reasons I chose to follow the lead of Pierce and others and use a 
translational semantics.  I didn't want to get hung up in the tedium of 
a subject-reduction theorem and hoped that I could rely on the reader's 
knowledge (and intuition!) about the polymorphic lambda calculus to 
simplify my exposition.  In particular, I have been somewhat dismayed 
that the operational semantics has gotten much harder to read as the 
details of the subject-reduction proof have been perfected.

So, if you want a proof built on rock-solid operational semantics, I 
suggest that you take a look at the paper on-line.  However, you might 
first look at the translational semantics in the book for a better 
pedagogic motivation of the semantics.

By the way, my book did not include the soundness of the language NOOL, 
introduced in chapter 18.  A paper with detailed operational semantics 
and type-safety proof of LOOM, a very similar language, will be 
forthcoming when we get a chance to finish revising the paper. 
Meanwhile a conference version of the paper, Subtyping is not a good 
``Match'' for object-oriented languages, with Fiech and Petersen, is 
available on the web page referenced above (though the journal paper 
semantics will be somewhat different).

Finally, let me make a quick response to Matthias' question about false 
claims modified on the basis of semantics:

William Cook wrote a paper in ECOOP '89 pointing out type holes in 
Eiffel, including those based on the "like Current" construct, which is 
very much like MyType (except not statically type-safe).  Cook et al 
then showed in POPL '90 how to model a MyType construct in a type-safe 
way in the polymorphic lambda calculus.  Since then I've explored how to 
incorporate this into a high-level language and provided static 
type-checking rules (see my book).  While no major language (aside from 
Eiffel) has picked this up in its strongest form (and they have not 
fixed the type-checking rules in ways many of us had hoped -- they've 
done other things instead), I have hopes that someday such a construct 
will be adopted in a major language.  I also don't believe believe that 
one could get the type-checking rules correct for such a construct 
without a strong understanding of semantics.  So, at the moment, there 
is no "success story" here, but instead some pointers for future 
language designers.

I believe there is also some work on making Beta statically type-safe 
that may be relevant here, but I'll leave that to others more 
knowledgeable about Beta.