[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