[POPLmark] Meta-comment

[Karl Crary]

Perhaps we're arguing semantics, but let me press a little bit more.  
Would "Dan's unsoundness" in Cyclone be an example of something 
trivially fixed?  It seems rather subtle to me.  I don't know if it 
actually was uncovered by a safety proof, but it certainly would have.

    -- Karl


Greg Morrisett wrote:

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