[POPLmark] The purpose of challenge problems?

[Benjamin Pierce]

Continuing a previous discussion... :-)

> It's struck me that there's been a bit of a disconnect in the last
> week's discussion of new challenge problems.  I think the issue is  
> that
> we are not in agreement as to their purpose.  So I'd like to ask the
> question, what is the purpose to a new challenge problem?

For me, there are two main motivations for thinking about new  
challenge problems:

1) Several people (Randy Pollack, for example) have made the point  
that, in some sense, the POPLMark challenge as it stands may be too  
*easy*.  Although it's got non-trivial binding problems and some  
slightly intricate inductive proofs, there may be other binding  
situations (dependent records have been mentioned as an example,  
IIRC) that will stress terms-with-binding representation strategies  
significantly harder than Fsub does.  Since representation of binding  
keeps appearing as a key issue in formalizing POPL-like proofs, this  
would be nice to know more about.

2) Looking beyond variable binding, one might wonder how various  
proof assistants fare on a broad range of tasks that come up in POPL- 
ish reasoning.  Inductive proofs are the bread and butter, which is  
why the original POPLMark  Challenge focused there, but one also  
wants to know that one's assistant will be good for co-induction,  
logical relations arguments, combinatorial reasoning involving  
significant numerical manipulations, algebra, etc., etc.

Of the two, (1) is both more immediate and better delimited, so  
perhaps it is good to focus there.  But it would be even nicer to  
identify problems with aspects of both 1 and 2 -- this was the reason  
for thinking about things like pi-calculus.

Regards,

      - Benjamin


> 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.
>
> So what would be the purpose of a new set of smaller, easier problems?
> I'm not sure.  Perhaps they are just for fun, in which case I'm simply
> being a killjoy.  But I don't see any way in which they advance our
> state of knowledge about the area.
>
> There's also been talk of proposing another Poplmark-sized challenge,
> exercising a different set of issues.  How profitable that would  
> depends
> on how well the selection of features is made.  But it seems clear in
> any case that each iteration tells us less.
>
> 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.
>
>     -- Karl
>
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark