[POPLmark] The purpose of challenge problems?

[Karl Crary]

That's a good point, but most of the problems proposed here are intended 
to be difficult in some way, rather than good instructive exercises.  If 
you want the latter, Frank Pfenning has several exercises in his course 
notes, with solutions included in the Twelf distribution.

    -- Karl


Michael Hicks wrote:

>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
>
>_______________________________________________
>Poplmark mailing list
>Poplmark at lists.seas.upenn.edu
>http://lists.seas.upenn.edu/mailman/listinfo/poplmark
>
>  
>