[POPLmark] Meta-comment

[Karl Crary]

You've made this claim a couple of times now.  I thought I refuted that 
implicitly in my earlier message where I listed several advantage of 
Twelf that had nothing to do with binders or higher-order 
representation, but let me say it explicitly:

I do not believe that the advantages of Twelf are limited to systems 
with traditional binding structure, or that make heavy use of 
higher-order encodings.  I say this on the basis of my EXTENSIVE 
experience with TALT.  A lot is going on in TALT, but the central focus 
are the machine's heap and register file, which are implemented using 
first-order representations.

Certainly Twelf was vital in the parts that did involve higher-order 
encodings.  (In particular, I find it hard to imagine doing the 
confluence proof, which is key to canonical forms, in any other 
system.)  BUT, Twelf worked very, very well for the main body of the 
proof, which was mostly first-order.  This was for all the reasons I 
listed in my previous message.  In short, I claim that Twelf works very 
nicely even when not exploiting higher-order representations.


Frankly, if you found that you haven't seen big benefits from Twelf on 
the Princeton FPCC project, it's because you are really using Elf, not 
Twelf.  The big breakthrough of Twelf is the meta-logical framework, and 
the Princeton project doesn't use that at all.  (Don't misunderstand, I 
know they have their reasons, to do with trusted computing base and so 
forth.)  You're complaining about the performance of your car when you 
won't turn on the engine.

So I don't really see that experience as relevant.  Princeton is 
basically carrying out the Automath program, using LF to construct the 
proof witnesses.  They use the Elf/Twelf proof search engine to help 
build the proof terms, and then they use an entirely different 
implementation of almost-LF to check them. (Incidentally, if Andrew is 
disappointed by how Elf/Twelf has worked, he hasn't mentioned it to me.)

    -- Karl




Daniel C. Wang wrote:

> HOL and Coq have had many past success in many areas that have nothing 
> to do with the handling of binders. Twelf is amazingly good at dealing 
> with binders. So amazingly  good that you can usally ignore all its 
> other deficencies. However, when dealing with binders is not a 
> significant part of the problem those deficencies become very apparent.
>
> I've also personally used Twelf on one very large project (FPCC) that 
> avoided higher-order encodings.  I  can say with hindsight that since 
> we were not using higher-order encodings it would have been easier to 
> use an LCF style system that built proof witness rather than to start 
> with Twelf.
>