[POPLmark] The purpose of challenge problems?

[Daniel C. Wang]

Proving any interesting theorem is a serious investment in time. I think 
the micro/macro-benchmarks should give people confidence that they 
didn't make the wrong choice at the get go. I'd currently choose a 
different system depending on my problem. At the very least the 
benchmarks should give people guidance about what choices they have. 
Hopefully, after some time people might start asking why there just 
isn't one way that "just works".

Karl Crary wrote:
> {stuff deleted}
> 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.
>