[POPLmark] Re: [Provers] Re: adequacy

[Geoffrey A. Washburn]

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/ --