[Prev][Next][Index][Thread]

the point of (any) semantics, was Re: semantics for F_{sub,rec} ??


Everyone -- I should clarify my reaction and my response to Thomas. 

1. I have done my share of semantics. 
2. I am doing my share of systems building. 
3. And I really wish that I could say 1 and 2 are related. 
   Naturally I understand that my students all share the 
   "cultural heritage" of my 'semantics phase.' But clearly 
   there should be more and if there is more, we can hopefully 
   bring semantics closer to others. 

So, I am calling on people to collect a bunch of examples with the
following characteristics: 

  - people make a claim about a language 
  - people later find that this is not true 
  - by adjusting the implementation to the language, we help programmers 
    develop, debug, and maintain their programs more easily and indeed, 
    prevent latent explosions. 

Example: I volunteer one of my own publications as an example. Some of 
you may be aware of my paper with Andrew Wright, which uses my 'evaluation
context semantics' to prove type soundness/safety for a series of ML-ish
languages. 

The last of the languages is the polymorphic ML core with call/cc. At the
time, plain polymorphic callcc had been added to SML/1e and people thought
'it worked.' Naturally our proof showed that it worked. We turned it into
a tech report and submitted it to Info and Control. 

Then I received an email message from Bob Harper with a short call/cc
program in the fragment of ML that we modeled. He asked me to run
it. When I did, it brought my SunView window manager down. Of course,
being a computer scientist I rebooted and ran it again. Lo and behold,
it did something weird again.  (I vaguely recall a complete crash.) It
then clicked in me that Bob (and Mark Lillibridge) had uncovered an
unsoundness in call/cc plus ML.

Andrew and I studied the proof and found that we had skipped one of the 
cases with "like the others." It wasn't like the others .. and it didn't
work.

I still claim that the four of us worked with semantic models and helped 
improve SML with call/cc to the point where programmers can rely on some
basic properties of the program once the type checker has blessed it. 

Perhaps others can contribute similar explanations (the Moscow ML
module system comes to mind) and Benjamin can collect the examples as
demonstrations of the usefulness of language models/semantics.

Thomas may wish to dig out uses of denotational (if there are any) 
semantics that have uncovered sand in our foundations and add them. 

-- Matthias
References: