[POPLmark] Meta-comment

[Karl Crary]

I sympathize with what Greg has to say, and I trust no one will be 
shocked that I think Twelf is exactly the right tool for that sort of 
thing.  Look, I don't own stock in Twelf, and I'm not promoting my own 
research.  I am strictly a user, and I've found--as a user--that Twelf 
is a terrific tool.

I now do nearly all of my meta-theory in machine-checked form, and it's 
not just me.  For all of our students, it's now de rigueur to do their 
development in Twelf, unless there's some reason not to.  This is not 
because we insist; it is because if it's feasible, it's clearly the 
right thing to do.  So while I understand that people are apprehensive 
about adopting a new way of doing things, it's not uncharted territory.  
At CMU we are doing it this way today.

I'm not going to claim that Twelf is perfect, because it's not, but I 
will say that I have hardly ever (only once, in fact) encountered 
obstacles I could not work around.  In fact, once you learn the ropes, 
things usually go smoothly.  I would say that the situation is already 
far from embarassing, and the tools are getting better all the time.

In my experience, when one does run into problems, it's never in the 
process of representing the logic.  Rather, it's in getting the proof to 
go through while working within the limitations of the Twelf 
meta-logic.  (This is why I'm eager for the conversation to move on from 
"can you do this or that in HOAS," because I've never once had trouble 
in that arena.  I suppose it's possible I've just been lucky!)

Since I'm sure someone will ask, I'll say what I've found the 
problematic limitations to be:  First, Twelf's meta-sentences are 
limited to Pi-2 form, which makes it impossible to do logical relation 
arguments in the meta-logic.  Second, Twelf will not let you manipulate 
the context in various ways that we find convenient on paper, which 
sometimes (rarely) necessitates baroque workarounds.  (Our Poplmark 
solution uses a fairly benign such example.)  Incidentally, Carsten 
Schuermann's upcoming Delphin system should ameliorate both problems to 
a great extent.

So that's my take.  I think that Greg and Benjamin's agendas are 
feasible *now*, as evidenced by the fact that we are already doing them 
at CMU!


P.S.  Greg, I'm surprised that you would say that you never learn 
anything from doing safety proofs!  I would understand if you said that 
reading a complete proof is rarely enlightening, but the process of 
putting together proofs has taught me plenty.  Indeed, I remember 
instances in work we've done together (TAL, Lambda-R, and especially the 
Capability calculus) where bugs in proofs led to important new insights!

    -- Karl