[POPLmark] Meta-comment

[Benjamin Pierce]

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

FWIW, I meant "do" as in me doing the gruntwork with the tool watching over
my shoulder, not "avoid" as in the tool doing it all by itself.  I'm not
that naive... :-)

For the rest, I don't see how to be much more specific than I've been.  I
want more than Greg does: not just type soundness proofs (though I agree
that already that would be a big step forward), but formalization of the
mathematical content of the majority of POPL papers.  I.e., I want a tool
that will greatly increase confidence in the correctness of mathematical
arguments across a range of specific topics in PL theory -- I want every
paper in POPL 2015 to come with a URL for a machine-checkable proof of its
main results.  

Regards,

    - Benjamin