[POPLmark] [Provers] Re: Adequacy for LF

[Benjamin Pierce]

> You are holding HOAS to a higher level of scrutiny when, so far, it is the 
> only technology that has been shown to be practical for doing this sort 
> of work.  It seems as though your preference is for systems in which 
> everything is possible and little is feasible, over a system in which 
> many things are both possible and feasible.

Here's my take on this.

It's not that anyone *prefers* deBruijn.  (OK, maybe Jerome. :-) DeBruijn is
horribly clunky.  But it has one huge attraction: you know you're not going
to get stuck.  Anything you can do on paper, you can do (with a lot of
annoyance, but no essential difficulties arising from the representation)
with deBruijn.  By contrast, what we've seen of Twelf is extremely
attractive in many ways -- many things seem to work impressively smoothly --
but the technology is much fancier and it's hard to get a sense of whether
it can be used (either "in principle" or "right now") to carry out the full
range of activities that we PL as folks are used to doing with our pencils,
or whether -- perhaps after sinking months of effort into getting used to
its way of doing business and developing hundreds of thousands of lines of
proofs in its style -- one might some day hit a wall and simply not be able
to do something that one really needs to do.

So I think all these questions about "but can it do this?" and "won't it
have problems with that?" should be viewed as people honestly trying to get
a clear understanding of the current state of knowledge about the strengths
and weaknesses of the HOAS / LF approach in general and Twelf in particular.

Regards,

      Benjamin