[POPLmark] Experience report with Twelf

[David Walker]

> > This underlines
> > something a point I've made before: it's a mistake to take the
> > paper design as written in stone when we start formalization.  If
> > we do that, we can fail to observe significant possibilities for
> > improvement that we would have discovered in the course of
> > formalization.

As we are language designers, it is often the case that we are designing the
language at the same time as we are formalizing it.  In this case, allowing
the logical framework to help guide the specification of the semantics is a
great idea.  (I like the specification of the pi-calculus that emerges from
Concurrent LF much better than most of the other specifications of the
pi-calculus I have seen...though that is another story...)

On the other hand, there are certainly situations in which the on-paper
formalization really is set in stone.  For instance, if a language already
has a specification and that specification is the basis for a variety of
implementations, you really cannot rewrite the spec as you verify it.  More
concretely, imagine the Department of Defense gives you the spec for their
weapon systems.  You are going to have to prove the adequacy of your
formalization with respect to the spec you are given, not some other
improved spec, no matter how much more elegant the new spec is.  In other
words, there can be a "legacy spec" issue.

Dave