[plt-scheme] Re: Expressivity gap between formal methods and PL's

Sorry I've dozed through most of this thread, but:

> Alloy is relational logic without an execution model.  It's
> declarative. You write your model declarative, write a couple of
> facts and that's it. FAR, FAAAAAAAAR, away from an 'executable' and
> generating an executable directly from an Alloy mode wouldn't even
> make sense.

In that case, it is just as well that we named our system Alchemy:

http://www.cs.brown.edu/~sk/Publications/Papers/Published/kdfy-alchemy-trans-alloy-spec-impl/

The paper shows how to generate an executable directly from an Alloy
model.  It has some nice twists such as automatically maintaining the
integrity of the models in the run-time heap.  And it *even* generates
... drum roll, please ... PLT Scheme code!

We have a paper in progress that further shows how to formalize the
relationship between specification and implementation.

Since this is pretty off-topic for this list, perhaps direct questions
about Alchemy should be addressed to Dan and Kathi (CCed) and me.

Shriram