[POPLmark] The purpose of challenge problems?

[Michael Hicks]

On Jun 1, 2006, at 2:27 PM, Karl Crary wrote:

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

One reason for smaller problems that appeals to me: there is some  
hope of completing the problem without a huge time commitment.   
Assuming the problems exercise ideas relevant to my interests, there  
is a greater possibility that I will be confident enough to try  
metatheory mechanization in the future.  The current challenge  
problems are basically non-starters for me given the amount of time  
I'm willing to put in (sad truth!).

I admit that this reason does not not directly address the research  
agenda, but rather argues for educating a mildly interested, non- 
expert, future user community.  While there is good documentation in  
many of these tools, having a motivated community of fellow users  
from whom to seek advice and ideas feels more reassuring.

But perhaps that's not the point of POPLmark.

-Mike