[POPLmark] Experience report with Twelf

Randy Pollack rap at inf.ed.ac.uk
Wed Aug 31 11:31:45 EDT 2005


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

Bob, David and Karl all seem to agree on this, and I do too.

The interesting new question in the present POPLmark discussion is how
the particular logic/checking tool chosen for the formalisation
effects the "significant possibilities for improvement" that we
observe.

Randy


More information about the Poplmark mailing list