[POPLmark] The purpose of challenge problems?

[Aaron Stump]

[ replying to Karl]

> The purpose of the original Poplmark challenge, as I understood it, was 
> to pose a problem dealing with an interesting set of language features 
> in order to see how well various technologies dealt with those 
> features.  Moreover, in order to keep the challenge from being too 
> artificial, the problem was selected to be one with some intrinsic merit.

As I remarked in the email that seems to have sparked this discussion, I
think that was a terrific goal which has been met with arguably very
good success.  A somewhat different goal, though one which we are
clearly all interested in, is devising approaches that make
formalization of PL meta-theory as easy as possible.  It seems to me
that going forward, POPLmark should work towards this goal.  My
suggestion is that smaller, easier challenge problems may be better
suited for this, because their smaller scale makes it easier to devise
for them not just a working solution, but as elegant a working solution
as possible.  My impression from the Fsub challenge problems was that
for many of us, it took all the effort we cared to muster just to get
something working using a particular approach.  The problems were too
complex to encourage playing around with different formalization
techniques.  But this kind of creative exploration is surely needed to
find techniques or, better yet, develop libraries for particular theorem
provers that ease the burden of PL meta-theory.

Aaron