[POPLmark] Meta-comment

[Daniel C. Wang]

Robert Harper wrote
{stuff deleted}:

> Third, I can certainly envision better tools, and they are coming 
> available as we speak, but for the moment Twelf is far and away the 
> best thing going.  It's there, it works well, we use it daily, and it 
> deals with the drudgery of metatheory in a way that no other tool that 
> I know of is capable of doing.  There is no fundamental need for a 
> radical new start, but we all agree that there are clear avenues for 
> improving on what we have.  

{stuff deleted}

I would like point out a design philosophy about Twelf that may make 
reasonable people want to start from scratch. The Twelf/LF approach is 
very nice to use because one can adopt an encoding style where the 
object logic concepts such as binding and substitution are encoded/reuse 
metalogic equivlents. The most of the tedium of defining your object 
logic is factored into the metalogic.. So only LF designers need worry 
about a whole class of problems once and users reap the benefits. This 
of course requires users understand how to reflect common notions of 
their object logic into the structure of the Twelf metalogic. Users are 
of course also "stuck" if the metalogic is not rich enough to reflect 
some of their object logic properties.  For example to encode linear 
logics in a way the reuses the binding of the Twelf/LF metalogic 
requires extending the notion of Twelf/LF function space to include 
linear functions.

Twelf/LF in nice because many things are "baked in". So long as those 
things are the right things to bake in everyone is happy. However, I 
think someone people are worried that they might want to step out of the 
what is baked in Twelf.