[POPLmark] Meta-comment

[Daniel C. Wang]

Benjamin Pierce wrote:
{stuff deleted}

>Of course, our current set of challenge problems is not exhaustive, and we
>do plan at some point to augment it with some additional challenges that
>bring out important formalization issues not raised by the current problems.
>But we also needed to keep things manageable for people that want to respond
>to the challenge, so we are not going to propose new problems until we've
>seen (a) what people can do with these, and (b) what small set of further
>challenges would have the best distinguishing power.
>  
>
I think, my complaint is that formulating requirements as challenge 
problems is counter productive. The poplmark spec should explicitly 
describe the requirements and then use the challenge problems only as 
concrete illustrative examples and test cases by which to preform 
concrete experiments. Or to say it another way, as a reader of the 
Poplmark paper, I ought to know if the benchmarks you've chosen are in 
fact good benchmarks for your goals. I do
think the paper as written allows me to make those conclusion. I think 
this ambiguity is making evaluation of the solutions difficult.

{stuff deleted}

>That's exactly the sort of information that I had personally hoped to get
>out of the challenge.  What I really want, ideally, is a single tool that I
>can use to do pretty much all the mathematical gruntwork of all my POPL
>papers.  If it's really true that all currently available technologies are
>"equally good or bad" from this point of view, then that's something very
>useful to know.
>
>  
>
Many people would like one single programming language that will pretty 
much do away with all their "programming grunt work". I think everyone 
here believes there is no single best programming language. I'd argue 
that a-prior there is no reason to believe there exists one best single 
system for avoiding mathematical grunt work. Given sufficiently specific 
contexts many reasonable people can be convinced that certain languages 
are obviously the path of least resistance. If I want to hack up a 
theorem prover or compiler I fire up SML. If I'm doing GUI hacking, I'm 
stuck with Java, C++, C# and the appropriate libraries.
 

>I'm not yet convinced that it's true, though.  To begin with, it's probably
>safe to say that some of the Twelf advocates would challenge your assertion
>that Twelf is just as bad as other approaches for most things. :-) Moreover,
>so far we've only seen two concrete answers to the challenge, and there are
>a few other representation techniques out there that also seem extremely
>promising -- for example, Christian Urban's nominal approach and Michael
>Norrish's method based on the Gordon-Melham axioms.  So I am still holding
>out hope that someone will give me something close to what I want.
>
>  
>
I believe the perhaps there's a system that will make *you* happy.  
Unfortunately,  think once that system is found it will not at all be 
clear why that system was the system that met your constraints.  Greg's 
description of his ideal system in a previous email is an example of a 
much more concrete set of goals and gives me a feel of what he has in 
mind. My claim is that the Poplmark as current written doesn't give me 
as clear an answer as possible.

A concrete exercise that I would find useful is for the poplmark authors 
to describe what sort of idealized system they would want by sketching 
solutions to the challenges using a fictional ideal system . Right now 
there isn't a clear "gold standard" by which to compare competing solution.

>The benchmarks themselves are indended to serve as the kind of use-cases you
>are asking for.
>
I'm really looking for something like Greg's previous email where he 
describes how  he imagines  he'd interact with the system.