[POPLmark] Meta-comment

[Robert Harper]

I was referring to the purposes of the POPLmark challenge, not to 
arbitrary theorem proving activities.  There is no question that the 
well-known theorem proving systems out there are better suited than 
Twelf for formalizing sophisticated theories of various kinds.  But for 
the purposes at hand I have so far seen nothing that can compete with 
the flexibility and utility of Twelf.  I presume that eventually some 
other solution to the challenge will be offered, but meanwhile we've 
solved ten other similar problems using Twelf in the course of our day 
to day work, with no particularly burdensome overhead and all the 
advantages of having checked every detail.

Bob

On May 11, 2005, at 8:01 AM, Peter Sewell wrote:

>
> Bob,
>
> 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.
>
> Our aim here is to expose both what can be done and what the
> limitations are.  Those limitations may be soft ("encoding XYZ is
> possible but just too much pain to work through") rather than hard
> inexpressivity results, and they'll vary depending on the user and on
> just what they're trying to formalise.  This isn't "picking at
> weaknesses", but trying to get a decent critical view of what's out
> there and of what's needed.
>
> Now, we're doing this as and for non-experts in the proof tools -- if
> one could quickly become experts in all of them then the challenge
> wouldn't be necessary.  Inevitably, then, we don't know well what
> those limits are.  We started with various guesses about things we
> thought are needed but would be tricky, and probably we underestimated
> what can be done.  Having got to this point, it'd be most effective
> for you (and the experts in the other systems) to enumerate useful
> formalisation and proof idioms, and their potential sticking points.
> That note with Karl is much appreciated; more in that vein would be
> very useful.
>
> Peter
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark