[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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