[POPLmark] Meta-comment

[Karl Crary]

Peter,

I believe that we demonstrate Twelf's practicality by the fact that we 
use it for nearly all of our work at CMU, and, so you don't have to take 
our word for it, by the fact that we were able to solve the Poplmark 
challenge without much difficulty.  I don't mean any disrespect to other 
systems when I say that to my knowledge no other system has demonstrated 
that it is ready for such use.  (I would be happy to be disproved on 
this point.)

The advantages of Twelf are not limited to higher-order abstract 
syntax.  The basic structure of Twelf lends itself to convenient proof 
development.  This is hard to appreciate without trying it, but I'll 
mention a few things that I have found important:

    (1) everything is done by pattern matching, there are no elimination 
constructs (that this is possible relies on a strong canonical forms 
property),
    (2) the induction mechanism is extremely lightweight,
    (3) the type/proof checker deals with most ancillary issues, so 
you're not burdened with auxiliary proof obligations,
    (4) term reconstruction spares you from repeating information that 
is well-determined,
    (5) binding, alpha-conversion, and substitution are handled with no 
overhead in most cases.

The upshot of all this is that nearly everything you write down is 
essential proof material.  I've worked with quite a few proof 
development systems, and Twelf is the only one for which I could make 
that claim.

    -- Karl


Peter Sewell wrote:

>It's clear that you are collectively using Twelf as a viable working
>tool, and much more so than I (at least) realized a month ago.  A
>greater awareness of what can be done there is a very useful outcome
>of this discussion.
>
>It is less clear how it compares with recent approaches in HOL,
>Isabelle, Coq, etc, and how you can argue that "there is, to date, no
>plausible alternative".  Each of those has some major advantages, the
>lack of which would be show-stoppers for certain applications.  For
>example, I'm thinking of network semantics work we've done in HOL,
>with Michael Norrish doing the HOL heavy lifting.  This needed some
>special purpose tactics and a lot of real and modular arithmetic; it
>didn't need dependent types.  I'm sure there are many other examples. 
>  
>