[e-lang] In support of formalization
david.nospam.hopwood at blueyonder.co.uk
Thu Jul 7 20:36:02 EDT 2005
Mark Miller wrote:
> Peter Van Roy wrote:
>> So where is the formal semantics of E?
> A start at an attempt can be found at
> <http://www.erights.org/e-impls/e-on-isabelle/Min_E.thy>. Having gone
> through this exercise, I find it did not at all contribute to my
> understanding of Kernel-E. Kevin Reid and Dean Tribble are both
> re-implementing Kernel-E. I would not recommend that they or anyone
> refer to this document to help clarify their questions about the
> definition of Kernel-E.
> Rather, the existing Java implementation is slow largely because it's
> heart is written to read like an executable specification of the
> semantics of Kernel-E. Programming languages are, in some ways, good
> formalisms to express the semantics of other programming languages.
>> Where is the kernel
>> language of E? Trying to define such a kernel language
>> will point out lots of little problems, I'm sure of it!
> The stale documentation that exists is at
I'm afraid I find this documentation to be totally inadequate. As an
example, <http://www.erights.org/elang/kernel/AssignExpr.html> does not
mention the expansion "v := x" => "&v.setValue(x)". Why not? If it
is just out-of-date, then some serious effort needs to be put into
updating it, and when changes are made to the language in future, the
documentation should be kept in sync.
> The heart of the
> Kernel-E implementation-as-executable-specification is in the "subEval"
> methods implemented by subclasses of EExpr, and "testMatch" methods
> implemented by subclasses of Pattern.
An interpreter is not a substitute for a formal semantics. Particularly
not when the language used to implement the interpreter (Java in this
case) is itself only defined informally, and is more complex than the
language being defined.
I strongly suggest looking at the Kernel-Oz semantics in Chapter 13 of
CTM as an example of how a semantics can be formal but clear, and give
additional insight into the language that cannot be matched by looking
at an interpreter.
I think part of the problem that leads some people to be dismissive of
formal semantics, is that they are thinking of the semantics as just
being a list of raw equations without explanation or motivation --
as <http://www.erights.org/e-impls/e-on-isabelle/Min_E.thy> largely is.
What should happen is that the *process* of formalization results in an
*explanation* of the language, that is more accurate and complete than
it would have been if developed informally.
David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
More information about the e-lang