[POPLmark] Meta-comment

[Daniel C. Wang]

Kevin Watkins wrote:

>On 5/11/05, danwang at cs.princeton.edu <danwang at cs.princeton.edu> wrote:
>  
>
>>Let me make this analogy with call-cc. One certianly does not need to use call-
>>cc at all, just CPS convert your entire program!
>>
>>Twelf allows for nice proofs, because it offers many advanced features that can
>>be used to encode object logics. Of course you don't have to use any of them,
>>but that just defeats all the reasons to use Twelf.
>>
>>Personally, If I wanted to use first-order encodings I might as well be using,
>>Coq, Isabell, or HOL. They are more mature than Twelf and I'd say more
>>appropiate for first-order encodings.
>>    
>>
>
>My inner snot can't resist pointing out that "mature" is as mature
>does.  Let's see a few solutions in the other systems Dan Wang
>mentioned, and compare.  There seems to be a lot of talk about other
>systems, and few complete solutions.
>
>  
>
Look, the POPLMark is not the only theorem proving problem in the world! 
Lets not forget that Coq has recently been use to reprove the four-color 
problem. (Google and I'm sure you'll find it.) Isabell/HOL now includes 
a full executable specification for a TCP/IP stack. HOL-lite is used to 
verify the correctness of the algoritms use in the x86 FPU. Lets see a 
Twelf signature that encodes the theory of the real numbers from first 
principles then we can talk. :)

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.

>Perhaps it's not worth mentioning, because it sounds as though Dan has
>made his mind up, but I'll point out that even setting aside HOAS, the
>LF (and therefore Twelf) method is quite different from Isabelle, say.
> In Twelf one writes, in an explicit notation, the computational
>content of the proof itself.  In Isabelle, which of the three Dan
>mentions I have the most experience with, one tends to write tactics
>that enable the Isabelle system to discover the proof, rather than the
>proof itself. 
>
Nothing pervents you from just using primitve proof tactics. Then the 
only difference one of natural deduction proofs vs sequent style proofs 
which too me are a wash.

> Although I have zero experience with Coq as a proof
>development system, it looks to me as though Jerome Vouillon's proof,
>at least, is in the latter style--I see tactics that presumably act on
>intermediate proof search states, rather than a concrete
>representation of the proofs themselves.
>
>  
>
Coq allows you to build explict proof witnesses similar to Twelf. The 
use of tactics is entirely optional. I'm personally netural on the issue 
of tactics vs proof witnesses. I think, it should be a non-issue.
{stuff deleted}