[POPLmark] Re: [Provers] Re: adequacy

[Robert Harper]

We should have a first draft of "How to Believe a Twelf Proof" ready 
very shortly.  Its intention is to provide the requisite background on 
the Twelf metalogic so that a reader or writer of a proof knows what's 
going on.  Contrary to what you're suggesting, there already IS a 
single source for this, namely Schuermann's PhD thesis.  To some extent 
I feel that we are being blamed for the ignorance of the audience, but 
I agree that a more concise overview may be useful supplementary 
reading to help people get up to speed.  No matter what the logical 
formalism, you have to learn it in order to use it ....

I'm reminded of the old, and out-moded, arguments about typed languages 
that boiled down to complaints about the error messages issued by the 
type inference engine of various implementations of ML.  The error 
messages don't make much sense until you learn what they mean.

Bob


On May 5, 2005, at 3:58 PM, Geoffrey A. Washburn wrote:

>
> On Tue, 3 May 2005, Karl Crary wrote:
>
>> For what it's worth, our students tend to understand LF much more
>> readily than Constructions.  I very much suspect cost of entry has 
>> more
>> to do with local experience than anything else.  So hopefully this 
>> very
>> discussion will improve LF's score!
>
> 	I think maybe one point that has not been emphasized enough is
>   that many of the difficulties that some people at Penn (and 
> elsewhere)
>   are having trying to understand the Twelf solution are not because
>   they are having trouble understanding LF.  I think everyone here
>   has a handle on the LF type system.  The problem is that in order
>   for a well-typed LF signature to be considered a proof, Twelf must
>   verify a number of properties about the signature (coverage, 
> totality,
>   termination, etc.).  The reasoning used by Twelf internally to 
> determine
>   whether a signature has the necessary properties is not easy to 
> grasp,
>   and to my knowledge there are no approachable resources for the
>   uninitiated that clearly explain the process and common pitfalls.
>
> 	Now in some ways it is comparing apples to oranges, but when it
>   comes to Coq, one only needs to understand the typing rules of the
>   Calculus of Inductive Constructions to determine whether a given term
>   is in fact a proof.  I theorize that the lay-programming languages
>   researcher has a much better understanding of how to repair a type
>   error in CiC proof term because they can inspect the type system and 
> see
>   exactly what rule they violated.  When Twelf gives a user 
> meta-logical
>   error, say "foo is not ground" or "Output of subgoal not covered", 
> the
>   LF type system cannot guide them in repairing their error.  And 
> again to
>   my knowledge, there is no single resource (aside from perusing the
>   source code) that explains the formalities of all the meta-reasoning
>   that Twelf does.
>
> 	Benjamin tells me there is an article "How to believe a Twelf
>   proof" in development, which sounds like it will hopefully help 
> others
>   understand what properties Twelf needs to verify.  However, based on 
> the
>   title I kind of expect this is directed at readers of Twelf proofs, 
> and
>   I think it would be valuable to develop a companion resource for 
> those
>   trying to develop proofs.
>
> -- 
> -- Geoff Washburn | geoffw at cis.upenn.edu | 
> http://www.cis.upenn.edu/~geoffw/ --
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark