[POPLmark] Experience report with Twelf

[Karl Crary]

Aren't you turning the matter entirely on its head?  Coq gives you no 
*benefit* to thinking about subordination, whereas Twelf does.  (To be 
fair, I don't think Coq can.  Starting from the Calculus of 
Constructions, I don't think you can define a reasonable notion of 
subordination.  But perhaps I'll be proven wrong.)

Setting that aside, now that you have some experience using Twelf, I'll 
bet that you will think about subordination ahead of time in the future.

    -- Karl


Stephanie Weirich wrote:

> 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
>