[POPLmark] Meta-comment

Tue May 10 15:51:45 EDT 2005

Karl has pretty well answered Greg's questions, but let me add a few 
additional points.

First, to reiterate, the situation is miles from "embarassing", unless 
you mean "embarassment of riches".  We here at CMU day in and day out 
use Twelf to formalize and check safety theorems for various languages. 
  For example, the cut elimination result and the equivalence result in 
the LICS paper with Murphy and Crary and Pfenning was completely 
formalized and checked by Twelf.  Subsequently we've investigated a 
classical extension of this language, and also studied typed 
compilation for it, all formalized and mechanically checked in Twelf.  
I could give many more examples.  There is no issue here, in the main: 
we can, and do, check these proofs mechanically every single day for 
novel languages with novel features (we're not just re-doing MinML 
every day!).

Second, your mileage may vary, but I, for one, do learn from doing 
these proofs, whether safety proofs for an object language of interest, 
or proofs of type preservation for compiler transformations, or proofs 
of cut elimination, or what have you.  The failure of these proofs is 
always instructive, and I, for one, do find deep and serious mistakes 
by trying to carry out these proofs.  Several times this semester 
alone, Karl and I, in work with our student Tom Murphy, have uncovered 
serious design flaws in plausible designs for a compiler for our 
distributed modal language because the attempt to formalize the 
argument in Twelf broke down.  The effort told us what was the problem, 
and helped us formulate a solution.  In some cases we simply needed 
some ingenuity to get around the limitations of Twelf, but in other 
cases we discovered we didn't know what we were talking about.  Any 
theorem, once it's proved and checked, is boring and only confirms 
"what you already knew" once you already know it.

Third, I can certainly envision better tools, and they are coming 
available as we speak, but for the moment Twelf is far and away the 
best thing going.  It's there, it works well, we use it daily, and it 
deals with the drudgery of metatheory in a way that no other tool that 
I know of is capable of doing.  There is no fundamental need for a 
radical new start, but we all agree that there are clear avenues for 
improving on what we have.  For example, the ability to impose 
structural congruences other than alpha conversion would be great.  It 
would be good to have a substructural framework so that we can better 
model state (we can do it now, but it's more painful than it ought to 
be).  It would be great to be able to model concurrency more naturally 
than is currently possible.  We have paper solutions to both of the 
last two problems, but the systems have not yet come on line.  There 
are other clear paths for improvement (better modularity, more direct 
representation of functions, etc).

The important thing is that these improvements are a natural evolution 
of what we have, and not a fresh start or a repudiation of the LF/Twelf 
methodology.  This gives me great confidence that, to the extent 
reasonably expectable, everything we do today will continue to work and 
be useful tomorrow, perhaps in a slightly jazzier or more elaborate 
form, but not fundamentally different.  For me this is the most 
important point in all of this discussion.  Yes, one can find 
weaknesses, and, yes, one can continue to find problems that either 
have never been tried or currently have no good solution.  This is not 
what is important!  What is important is that we have established a 
solid beachhead with a clear path for improvement, and that there is, 
to date, no plausible alternative.  It's well and good to pick at 
weaknesses, it's quite another to propose a viable alternative.

Finally, it is a disservice to the community for us to continually 
berate ourselves for our shortcomings even in the presence of such 
great achievements.  It is not only technically wrong to proclaim 
ourselves to be in an embarassing situation with respect to 
formalization, but it is also deeply counterproductive to the aims of 
the field.  Our colleagues outside of the area should get the message 
that there's TONS that we can and do do, every day, not that we're 
bogged down with things that we cannot do (yet).  It's fine for us 
within the field to snipe at each other, criticize one another's work, 
strive to do better, but we should not lose sight of the big picture of 
achievement that we should all be very proud of.

Bob

On May 10, 2005, at 7:55 AM, Greg Morrisett wrote:

>> 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
>
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark