[E-Lang] Syntax change: reducing side-effects

Mark S. Miller markm@caplet.com
Mon, 12 Feb 2001 01:32:28 -0800

At 08:40 PM Sunday 2/11/01, Vijay Saraswat wrote:
>BTW, has any one thought through a static type-structure for E?

No, and I can't imagine anyone I'd rather see try.  I did attempt to design 
the language so this would be feasible, but I'm too ignorant of type theory 
to have any confidence that I succeeded.

In any case, my stance on E and static type checking is the lint philosophy. 
E itself accepts and runs any programs that meet its relatively weak static 
acceptability criteria, which include some interesting stuff (auditors), but 
does *not* include static type checking.  As a shell and rapid prototyping 
language, we need to keep it that way.

External tools should be able to do as good a job inferring types from E 
programs as they do for, for example, Scheme or Smalltalk programs.  In 
addition, E's guards can often be safely understood as static type 
declarations, potentially making the job of a type inferencer much easier.

Different such tools can apply different static type theories, and thereby 
accept or reject different sets of programs.  A particular project or 
programming shop could adopt one it likes, and only allow passing programs 
to be committed to the shared source tree.  This would provide all the 
reliability advantage of static types enforced by the language, while still 
allowing the programmer to run and debug private versions that violate these 
constraints, enabling more rapid experimentation.

In any case, as far as normal type theories are concerned, the only thing 
they're protecting you against is a runtime occurrence of 
"MessageNotUnderstood".  Why should we care?  If this particular surprise 
happens at runtime, at least it's fail-stop, which is vastly safer than 
other things we worry about.  Also, actual experience with Smalltalk says 
that these don't happen too often, and it's not too hard to beat them out of 
a program with runtime debugging.  Conventional static type checking is like 
painting the Titanic -- a fine thing to do once greater dangers have been 
taken care of.

In any case, I'm much more interested in the design of 
static-type-checking-like systems for statically catching security mistakes, 
especially mistakes made under maintenance.  In this regard, see MarcS's 
thought provoking http://www.skyhunter.com/marcs/trustrule.htm and our 
earlier thread on the "suspect" & "rely" declarations.  I strongly suspect 
that the impressive formal machinery created by type checking folks can be 
retargetted to this far more important problem.