[e-lang] In support of formalization

[David Hopwood]

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 
> <http://www.erights.org/elang/kernel/index.html>.

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>