[POPLmark] Meta-comment

[Peter Sewell]

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