Exciting week!

I've had an exciting week in Amsterdam, attending XTech 2006 thanks to the generosity of Mozilla. On Thursday I visited Eelco Visser and Martin Bravenboer at the University of Utrecht. It was a fun and productive visit.

In the last couple of months I have started using Stratego/XT to model the semantics of ECMAScript. I believe that it's possible to scale the semantic frameworks that we use in research up to model whole, industry-sized programming languages. Now, these modeling frameworks are formal systems, just like programming languages themselves. So it should also be possible to express these models in a machine-executable form. There are several benefits to this approach:

1. The added rigor that comes from the level of detail and precision required to get a machine to understand the model.
2. The ability to test actual ECMAScript programs against the model.
3. A reference implementation against which implementations can be tested.
4. The eventual possibility of applying automated reasoning tools to the model (though not immediately!).

A particularly attractive feature of Stratego is its extremely customizable syntax. I have been able to use this to be very particular in defining the "syntax of the semantics" to maximize its readability.

Eelco and Martin liked my model--they found the CEKS machine representation of continuations lovely--and are glad to have an interesting application of Stratego. We talked about some of the things I could do better (and they already found a few subtle bugs in my implementation) as well as a couple of requests I had for Stratego. They're interested in what kinds of optimizations they could apply to their compiler that would provide the most benefit to applications like mine. For instance, since my abstract machine generally operates on only a few small forms that have fixed shapes, deforestation might be applicable.

Martin is now working on implementing the ECMAScript grammar, which is notoriously difficult to express in traditional parser generation frameworks. The module grammar formalism SDF, based on Tomita's generalized LR parsing algorithm and used in the Stratego/XT system, should actually allow us to define the syntax quite elegantly. This will allow us to parse actual ECMAScript programs, as well as to model eval realistically, since it relies on parsing strings as ECMAScript programs.