[POPLmark] Meta-comment

[Greg Morrisett]

Karl Crary wrote:
> P.S.  Greg, I'm surprised that you would say that you never learn 
> anything from doing safety proofs!  I would understand if you said that 
> reading a complete proof is rarely enlightening, but the process of 
> putting together proofs has taught me plenty.  Indeed, I remember 
> instances in work we've done together (TAL, Lambda-R, and especially the 
> Capability calculus) where bugs in proofs led to important new insights!

Let me clarify here:  I don't recall that I ever uncovered a "bug" in
the source typing rules that I initially set up.  By "bug", I mean
something that wasn't trivially fixed --- something that I thought
should be sound that for some deep reason, wasn't.

In contrast, I've found lots of bugs in typing rules for intermediate
states, and lots of bugs in induction hypotheses that are too weak.
And most of my effort in a soundness proof is getting these details
right.  In turn, this may make me re-forumlate the source typing
rules to simplify the proof.

-Greg