[POPLmark] The purpose of challenge problems?

[Michael Norrish]

Karl Crary writes:
 
> So I would like to suggest an alternative challenge problem: Use the
> system of your choice to formalize your own work.  This challenge is
> natural, and is guaranteed to exercise the features of interest to
> you.
 
> Clearly this is the future of the area, so is there any reason why
> we shouldn't get on with it?  Challenge problems are fun, but I
> would much rather read about real results.

My take on POPLmark is that it was an opportunity to show people
currently outside the fold that our systems are indeed something
they'd like to use.  POPLmark was a call by a bunch of non-system
users: "We think we might want to use mechanical tools; show us what
you've got!"  In turn, wouldn't it be nice if our tools did reach the
point where people submitting to POPL were happy, indeed eager, to put
mechanised versions of their papers up on the web, or in an appendix?

That's why the original authors gave themselves the invidious task of
marking submissions.  They were (are?) 'outside the fold', and so in a
reasonable position to judge whether or not they might like to use our
technology to do mechanised reasoning.

For this reason, turning inwards and formalising our own work (though
separately interesting I'm sure), has very little to do with POPLmark.
We know we can formalise stuff.  And our own standards are not those
of POPL authors: our own methodologies of choice look completely
natural to us, even if they may look alien and incomprehensible to
others. 

I like the idea of micro-benchmarks.  They give us an opportunity to
test whether or not our systems are up to scratch in a variety of
small and self-contained ways.  The point is not so much to prove the
particular theorem, but to do so in a relatively self-aware manner,
thinking as one does so, "Would anyone other than an expert want to do
this?  If not, what does this tell me about my system, and how might I
improve it so that non-experts might use it?"

Michael.