[POPLmark] Experience report with Twelf

[Stephanie Weirich]

Hi Karl, thanks for the reply!

>
>> 3) HOAS, non-modularity and strengthening
>>
>>
>>
>
> I think Michael has already shown how to make this issue go away in  
> your proof, but I wanted to make a larger point.  I believe that  
> issue arose at all only because you made the class table (which  
> includes all the code) a parameter to everything, thereby making  
> exp subordinate to other types that it shouldn't be subordinate  
> to.  A better design would be to make the subtyping relation the  
> general parameter, and then check that the subtyping relation is  
> compatible with the class table.  If you did that, you wouldn't  
> have had the problematic subordination edge in the first place.
>
> That's not the point.  The point is that a language design that  
> seemed perfectly reasonable on paper turned out to be subtly flawed  
> once we went to formalize the metatheory.  This underlines  
> something a point I've made before: it's a mistake to take the  
> paper design as written in stone when we start formalization.  If  
> we do that, we can fail to observe significant possibilities for  
> improvement that we would have discovered in the course of  
> formalization.
>

Certainly, I'm willing to change a language design to better suit my  
proof assistant. In fact, I made several small modifications to the  
specification to make things easier to prove.

But, if a *particular* proof assistant (and language representation)  
is going to require me to modify my specification, I'd like to know  
about it ahead of time. My Coq proof did not require as significant a  
modification to the specification of FJ as you propose. (Nor do I  
think your modification would significantly improve my Coq proof.) In  
my original email, I was listing the reasons why I preferred Coq to  
Twelf in this particular instance---the fact that I didn't have to  
deal with subordination, either by modifying my specification, or by  
carefully crafting my proof, is one of them.

--Stephanie