[POPLmark] Experience report with Twelf

[Robert Harper]

I think it would be a grave error to attempt to take on such a job.  I 
don't believe that the "throw it over the wall" model can ever be an 
effective way to proceed; you're just setting yourself up for failure.

Bob

On Aug 30, 2005, at 3:04 PM, David Walker wrote:

>>> 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
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark