[POPLmark] Meta-comment

[Karl Crary]

Hi Greg,

I think "Dan's unsoundness" in Cyclone is a perfect example.  Okay, you 
didn't happen to find it by doing the proof, but you would have found it 
sooner if you had done the proof.  A similar case arose in TALx86 with 
exceptions and templates, if I recall correctly.  There's also the 
conflict you mention between old-style ML polymorphism and continuations.

In all of these cases, two things that work fine in isolation are 
unsound when they're put together.  To find these cases, if we're not to 
trust to luck that we'll find them by accident, we carry out the proofs, 
and we learn when they fail.  (Indeed, as you point out with runST, we 
sometime learn even when they succeed.)

I think the reason that we tend to see this when combining features, and 
not when working with single features in isolation, is that for simply 
core languages we are capable of running through the proofs and 
isolating the important (ie, interesting) issues in our heads.  When we 
go to write the proofs down, we usually have dealt with everything but 
the niggling details.

In that sense I agree with you, it would be great if we no longer had to 
read proofs that revealed only niggling details, and machine-checked 
formalisms are great for that.  But I think that's only a minor payoff.  
More importantly, machine-checked formalisms make it possible for us to 
attempt proofs that we couldn't before.

For example, Bob Harper, Michael Ashley-Rollman and I have recently been 
working on formalizing the entire meta-theory of Standard ML.  This is 
something that we never would have contemplated without Twelf.  And, I 
must say, we've learned a lot by doing so, and not all of it about Twelf.

One thing that's come out of the experience is the realization that 
comparing Twelf (or any other machine-checked formalism) to pencil and 
paper is unfair.  The real comparison is between Twelf and Latex, since 
no pencil and paper proof is publishable.  In my experience, the size of 
the Latex source and the Twelf proof of the same theorem usually are 
roughly comparable.  The Latex proof only wins because we omit so much 
detail.  (And often that omitted detail is wrong, such as the several 
bugs that Jerome has found in the Poplmark challenge's paper proofs.)

    -- Karl




Greg Morrisett wrote:

> Karl Crary wrote:
>
>>
>> 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.
>
>
> I'm sure you're right that a proof would've found this, but that's
> not how it happened.  For one thing, we left the combination of
> & and existentials out of the model.  When you're doing proofs
> with pencil and paper, you try to cut things down a lot.
>
> Dan tripped across this problem for other reasons and then
> formulated two different "fixes" to the problem and then wrote
> a paper where he constructed a model and showed both fixes were
> sound.
>
> I would love to hear of examples where someone got deep into
> a subject reduction proof and decided that the underlying safety
> property they were trying to establish for a language was in
> fact just not true:  I'm thinking along the lines of the old
> ML imperative polymorphism + callcc/throw.  I mean, there's a
> case where the simply-typed case went through like a breeze,
> and the more complicated case just wasn't modeled but was assumed
> correct.  In my opinion, that was a rare occurrence.
>
> In contrast, I'm frequently stunned by a set of typing rules
> that I think must be unsound, but for some very cool or deep
> reason, turn out to be sound.  It's true that the proof provides
> a lot of reassurance and insight in these cases.  An example is
> something like runST in Haskell, where the rank-2 polymorphism
> and the indexed monad conspire to trap the "effects" of running
> a computation.
>
> -Greg
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>