[POPLmark] Meta-comment

[Greg Morrisett]

> The answer to both questions I would say heavily depends on what you 
> want to do with the formalized metatheory.
> Unfortunately, the whole challenge is a bit vague about the issue. 

I'm not sure what the POPLmark folks believe, but here's what I
think is the most pressing need:  getting subject-reduction proofs
out of papers.

As an author, I mess these up all the time.  One of Zhong Shao's
students just found a bug in the TAL chapter of Benli's latest
book.  It's minor, and doesn't invalidate anything at the meta-level,
but it's precisely the sort of bug that is caught by mechanization
(this person is doing it in Coq.)  Also as an author, I somehow
resent having to burn pages on a proof that is essentially write-
only.  I would much rather put in a URL and invite any untrusting
reader to download and verify the proof with the aid of a machine.
Then I can concentrate on the key things -- the set up, the
induction hypotheses, etc.  Finally, it's kind of annoying that
in the past 10 years, not once has one of my type-soundness
proofs uncovered an insight into the underlying problem.  Rather,
it's simply  served as a cross-the-t's, dot-the-i's sort of check.
But just try to publish a paper in POPL, ICFP, LICS, etc. where
you don't include the proof (sketch) or at a minimum, the URL
to the write-only tech report...

As a referee/reviewer, I *really* don't want to see another
subject-reduction proof.  It's very frustrating to pour through
one, knowing that very few readers will actually read the proof.
It's doubly frustrating when you realize just how bad humans are
at doing these checks.  It's the moral equivalent of me checking
over someone's proposed source code, which has yet to be run
through a parser, much less a type-checker.

To me, it seems somewhat frustrating that a subject-reduction-style
proof is so "turn-the-crank" in terms of pencil and paper, but
still rocket science when it comes to mechanization.  We're not
talking logical relations, fancy notions of bisimulation, or
correctness --- just proving that a property is preserved by
evaluation and that it implies progress.  Nevertheless, there is,
in my opinion, no environment that scales to oh say, the original
TAL paper or all of Benjamin's 1st book.  Oh sure, with heroic effort
someone can do it (cf TALT),  but that's the point -- it shouldn't take
heroic effort.

So in short, I think the most pressing application is an environment
that would allow me (not the brightest bulb on the list) to knock
off the last 10 years of POPL *subject-reduction* proofs.

Now of course, there are more lofty goals that you mentioned,
ranging from program specification & verification, reasoning
about deeper properties of programs, to automatic code extraction.
But let's face it, it's EMBARASSING for the field that we can't
even mechanize the *simplest* formal property of languages,
especially when, on paper, the task is so....mechanical.

What I dream of is a system that lets me easily:

* define my abstract machine:
   * syntax, including binding and congruences
      * ideally, in a syntax similar to BNF?
   * evaluation relation
   * NB: no need for open worlds, but things like
     mutually recursive bindings in a heap or records
     or modules need to be covered.

* define my evaluation relation

* define my typing relations

* write down substitution lemma, press button and
   have system automagically discharge the lemma.

* write down canonical forms lemma, press button and
   have system automagically discharge the lemma.

* write down preservation lemma, and do the interesting
   reduction rules, while the system takes care of the
   congruences.

* write down progress lemma, and do the interesting
   reduction rules, while the system takes care of the
   congruences.

-Greg