on semantics, specification, metacircularity, \JS, etc.
sk at cs.brown.edu
Fri May 21 06:37:07 PDT 2010
The recent thread about specifications and meta-circularity devolved
into a discussion about semantics. Before one can argue whether or
not the standards committee should invest effort in helping out (much
less incorporating) a semantics, it helps to understand what form a
*useful* semantics can take, and how much (in this case, how little)
the committee needs to do to help the semantics along.
First I want to summarize the semantics effort from my group at Brown
(Arjun Guha, Joe Politz, Claudiu Saftoiu, Spiros Eliopoulos), because
I don't think it has been represented accurately, and the details
really matter to this discussion. The semantics comes as a bundle of
software tools, tests, and other mechanized and executable artifacts,
all of which are here:
This effort is meant to be a bridge between practitioners and
researchers. In particular, practitioners want and need tools that
work on actual source programs in the wild, not just on cute little
abstract artifacts; some researchers (like us) need the abstract
artifact but also want it to conform to reality.
(NB: This is not meant to be a coded criticism of the work of Taly,
Maffeis, and Mitchell, whose semantics effort is heroic. Both groups
are aligned in wanting to build the same kind of bridge; but we differ
enormously in our choices of media and means of construction.)
===== The Origin of the Semantics =====
First of all, why did we build our semantics? Our goal wasn't to
build a semantics -- it was (and is) to build real tools that work on
real programs. We built three different tools:
- a very rich flow analysis for use in Ajax intrusion detection;
- a static type system;
- a different flow analysis for use in the type system.
By the end of this we got very frustrated because it's very hard to
build tools for a large language, and it was impossible for us to
state anything formal about what these tools did.
This forced us to split the language into syntactic sugar and core,
and re-build all our tools atop the core. This has *tremendously*
simplified and accelerated our work -- both re-implementing the above
tools and creating new ones. Ultimately, all these tools run on real
checkers that verify the properties of ADsafe by operating on the
actual ADsafe source code.
===== The Structure and Guarantee of the Semantics =====
As I said, our semantics splits the language into a small core and a
desugarer. The core (\JS: read "lambda JS") is small (fits on the
proverbial page, at least A4 <-;) and is designed to support the
proofs researchers do. Desugar is much larger, but it is a
combination of mostly small pieces that are also amenable to study.
So we have two functions, desugar and \JS. For a program e, we can
run \JS(desugar(e)) to obtain an answer. But does this have any
evaluator like the one in your favorite browser. We show, for a
produce the SAME ANSWER. That is, the semantics is (nearly) every bit
as tested as your browser's evaluator itself is!
This now yields a strategy for researchers to have impact on practice:
develop your work atop \JS; if you ever want to run it on a real
source program, use desugar to convert the source into \JS; you can
now have very high confidence in your result, since we commit to
maintaining confirmity with the browser test suites.
===== Presentation of the Semantics (where Metacircularity Goes) =====
Some prior messages have assumed that developers are incapable of
reading a semantics (I'm going to sidestep this very condescending
assumption) and, implicitly, that there is only one way of writing
one. This is not true at all.
Each of the artifacts above can be written in a variety of ways:
- as a set of transformation rules on paper
- in some funky term-rewriting language (Maude, XSLT, ...)
- as, say, a Haskell program
- as a set of semantic rules on paper
- using a mechanization of those rules (eg, PLT Redex)
- as an interpreter in, say, Scheme
- Because each strategy offers strengths and weaknesses, there's value
to having more than one description of each layer. (Conformity
follows from testing.)
- The two layers don't need to be written in the same language: the
surface syntax of \JS defines the interface between them. Systems can
fruitfully use implementations of each layer in different languages.
Observe that in this world, metacircularity is just one of many ways
of presenting the system. Personally, I think using a metacircular
interpretation as a way of understanding the language is both
misguided and under-defined, but that is a separate point that I won't
get into here. More importantly for those who are really attached to
that idea, it is perfectly consistent with this semantics strategy,
and it lives in harmony with others.
===== The Relationship to Standardization =====
Finally, what does all this have to do with standardization?
Proving properties of systems is not the business of the
standardization committee. However, a committee can decide that it is
*sympathetic* to this goal, and wants to enable it. It can do so in
1. Working with practicing semanticists can be of real value. For
instance, we are currently migrating desugar and \JS to ES5; this has
been a very interesting exercise, and we are struggling to find the
right locus for certain decisions. This experience might be of value
to the standardizers. In short, the standard and a semantics can
potentially grow symbiotically.
2. But if the standardization committee wants to have nothing to do
with formal semantics, that's fine, too. In that case, the most
valuable thing you can do is commit to maintaining conformance suites.
Our re-design for ES5 is using the Conformance Suite to guide our
work: think of it as a test-driven development of the semantics.
Thus, I hope this message contains at least one surprise for those
working on ES5 standardization: you may have assumed that hardening
builders; we're here to say it is *just as valuable* to pointy-headed
semanticists, at least ones who use a semantics strategy like ours.
I appreciate your reading this far, and we value your comments.
More information about the es-discuss