[POPLmark] Experience report with Twelf

[Karl Crary]

Hi Stephanie and others,

I'm coming into this discussion late, but I wanted to make some remarks 
about this:


Stephanie Weirich wrote:

>1) No polymorphism for logical operators
>
>  
>

I really don't think this is a serious issue, at least once one gets 
used to Twelf.  The sort of equality-utilization lemma you refer to is 
quite typical, and I don't find it troubling at all.  With the help of 
an emacs macro, I can define and prove those lemmas in just a few 
seconds; not much more time than it would take to run a tactic.  Of 
course, that's only the first time; after that you have the lemma available.

The upcoming module system is supposed to eliminate the need for this, 
but frankly, I find polymorphism to be such a non-issue that I'm not in 
any special hurry for it.


>2) Constructive logic and logic programming
>
>  
>

I'm fairly suspicious about this point.  Classical logic really 
shouldn't be helping you in any significant way, and if it is, I suspect 
you're proving the wrong thing.  In this case, I think that either your 
operational semantics is mis-specified or your safety proof is 
incomplete, depending on what viewpoint you want to take.

Type safety means that a well-typed program will execute successfully 
until it terminates.  This means that if the program has not terminated, 
then a transitition exists and a machine can find it.  Usually the 
specification of the operational semantics makes it obvious that a 
machine can find whatever transition that exists, so we focus 
exclusively on the former.  However, if the operational semantics 
requires the machine to decide an undecidable problem, than that 
language is *not* type safe.

So I claim that either your operational semantics should explicitly give 
an algorithm for deciding subtyping, or you need to prove that subtyping 
is decidable.  Either way, classical logic won't be of any help.

(As an aside, I'm also suspicious of the semantic foundations of 
classical Coq.  The semantics of the Calculus of Constructions are 
completely well understood.  For Inductive Constructions they are a lot 
less accessible, but I believe they are also well established.  Of 
Induction Constructions + excluded middle I know nothing -- but perhaps 
someone will give me a reference.)

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


>4) Bottom-up vs. top-down
>
>  
>

The %trustme directive is implemented in the latest CVS version.  That 
should give you what you want.

    -- Karl