Lambda the Ultimate

The essence of Alloy as I understand it is that you specify some model of your piece of software as well as properties that must hold, then Alloy works to see if there are any examples where the model fails to satisfy those properties. So it can't prove anything per se, only make the process of showing that some manner of property or "theorem" about the model is false.

In short, you can't use Alloy for PL design as you seem to want. For formally modelling a programming languages I suggest you check out Coq, Twelf, or perhaps some variant of HOL. Look at the old thread on the Poplmark challenge for some good ideas on where to start.

It looks like Alloy will be good at modeling user level interactions and abstractions. There are references in the book to modeling Undo-Redo, a mail package address book, and similar structures one might find in designing an API/Protocol that would underly a modern GUI. So I can definately get a lot of milage out of Alloy in that regard.

But I also want to model the programming language in which such structures would be implemented. It might be possible to use Alloy to spec out a high level design for a PL and then move on to another tool as the design becomes more concrete. With that approach Alloy's inability to develop proofs wouldn't be too great an obstacle to surmount. It would be more a question of mapping between Alloy's modeling language and that of the proof development tool.

Indeed, Jackson makes a strong case for what he calles "The Small Scope Hypethesis" which is that while Alloy can't find a proof, it can find a counter example within a bounded search space which in practice provides vastly greater coverage than one would achieve with hand crafted testing and that for any given flawed design one should be able to find a counter example within a small enough scope for the problem to be highly tractable on modern hardware.

In Alloy the scope is the number of entitites in each set represented in the model, so one could search all permuations of address book operations possible given say 1 address book, 10 email address aliases, 10 actual email addresses, and 10 email address groups. Apparently Alloy avoids combinatorial explosions by collapsing similar cases to heavily prune the search space.

The hypothesis seems reasonable and should lead to a sound design at which point the challenge becomes one of verifying the design implementation.

In any case, in addition to a good tool to work out user level API modeling, what I am looking for is a lightweight way to formalize the semantics for their implementation language (which would have mutliparadigm support and a new End User friendly syntax along the lines I've alluded to in past postings) and (if possible) prove that the implementation matches the semantics. For that aspect of things, I'll use a parsing expression grammer to capture the syntax and map that to Scheme code as an IR.

Again, I strongly recommend looking at the poplmark challenge link I mentioned in my previous post. I'd argue that for formallizing a programming language, Alloy's logic is inappropriate because it is relatively inexpressive. Out of curiosity, how would you try to encode the progress and preservation theorems of a statically typed programming language in Alloy?

I'm very curious about what your impression of twelf (which is in fact essentially designed for the sole purpose of encoding logics and programming languages, as well as being just powerful enough to encode a progress and preservation proof), and Coq (which is tool meant for formalizing mathematics in general, in addition to logics and programming langauges), as well as their respective approaches.

Thanks for all of the pointers! Since formal methods are new to me, I clearly have a lot of reading to do before commenting further!

Since Alloy emaphsizes a lightweight nature that allows one to dispense with many proof generation details I decided to start with it on the assumption that it might work for my modeling needs outside the PL domain.

I can't say how I'd encode a type system in it. It may be feasible, it may not. Jackson claims a reasonable level of expressiveness. So after I've finished the book I should have a better sense of whether it could be adapted to cover a type system. In the meantime, I will take a look at the other systems you suggest.

Perhaps Alloy and twelf or Coq could be used in combination

There is a book on the Coq proof assistant, as well:

Interactive Theorem Proving and Program Development
Coq'Art: The Calculus of Inductive Constructions
Yves Bertot and Pierre Casteran

I just received both of them last week and have not had a chance to read either.

My copy should be arriving tomorrow or the day after; I'm very much looking forward to digging into it, and will gladly post a review when I do.

A few comments about the role of Alloy in PL design.

First, regarding checking versus proof. Alloy is indeed a model finder and not a prover, so it cannot prove theorems without additional help (eg, a small model theorem). But even in contexts that usually require proof (such as PL design), a model finder can still be useful. Why waste time trying to prove a theorem if a model finder can generate a counterexample for you automatically?

Second, regarding expressiveness. Alloy's logic is first order logic, plus relational operators (generalized over arbitrary arity relations) and transitive closure. FOL is more powerful than you might think.

Is Alloy the right tool for PL design? Probably not. It's not aimed at this area, unlike tools such as Twelf, and its relational logic is not a good match for higher-order functional languages. On the other hand, there's some fun (and maybe even some productive research) to be had in applying lightweight tools like Alloy to language design, and its semantics is a good match for object-oriented and relational languages.

The standard Alloy distribution includes a model for checking type soundness of a fragment Java (in Alloy 4, click on File | Open Sample Models, then select examples/systems/javatypes_soundness.als; Execute | Show Metamodel to see the syntax tree and semantic domains, and Execute | Check TypeSoundness... to check the theorem). Alloy's been applied in some other language settings; for example, Christie Bolton used Alloy to check the soundness of failures-divergences refinement for CSP.