[POPLmark] Meta-comment

[Greg Morrisett]

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