mathematical models

[Matthias Felleisen <matthias@cs.rice.edu>]

On the role of mathematical models: 

1. Mathematical models have helped physicists a lot for their study of
   properties of the real world and for describing to laymen what they
   find. I am (still) hoping that mathematical models will help programming
   language researchers to study properties of PLs and to explain
   programming languages in standards. We started out that way. In the
   early days, Schemers (speak Guy and Gerry) used interpreters as mostly
   mathematical models for this purpose.  Interpreters are okay to study
   some things but are probably ill-suited for many explanatory purposes.
   R3RS contains a denotational semantics. If take as such, it is too
   extensional for many purposes. If misinterpreted as an interpreter, it
   is equally ill-suited as an interpreter. Some of us have used rewriting
   models to validate properties of program transformations, type systems,
   garbage collectors, and other properties. They too suffer from
   problems. Different models are good for different purposes.

2. Should mathematical models be included in or should they be language
   definitions? ML is the only language (I know of) that has a fully
   mathematical specification. Is/was this experiment successful? I believe
   it failed for technical reasons. They too understood that a mathematical
   model couldn't be the only specification. They wrote a commentary.

   Did they _benefit_ from constructing and working with a fully
   mathematical model?  Most definitely. Their explanations of things (how
   ML works, how type checking works, what it accomplishes, what it doesn't
   accomplish, how GC can be extended beyond rachability) are often crisp,
   unambiguous, and accessible. Their new effort (sml1996, ml2000) benefits
   a lot from playing with mathematical models. 

I believe that a full-fledged model of Scheme (or several related models)
would help us formulate what the language provides, what properties it
should satisfy, etc. The model should be used to construct English
descriptions and to validate descriptions of ideas. It may accompany the
report or it may be available in the Scheme repository at Indiana. That
part is probably irrelevant. Having precise models of what we want to say
is important. 

-- Matthias