[POPLmark] Meta-comment

[Benjamin Pierce]

Hi Dan,

> 1. What is the current state of the art in formalizing language 
> metatheory and semantics? What can be recommended as best practices for 
> groups (typically not proof-assistant experts) embarking on formalized 
> language definitions, either small- or large-scale?)
> 
> 2. What improvements are needed to make the use of tool support 
> common-place? What can each community contribute?
> 
> The answer to both questions I would say heavily depends on what you 
> want to do with the formalized metatheory.
> Unfortunately, the whole challenge is a bit vague about the issue. In 
> fact, I know enough about HOL, Twelf, and Coq that I would recomend each 
> as a "best" solution for different problem domains. If we restrict 
> ourselves to some common "generic" problem domain. I'd say they are all 
> "equally good or bad".

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.

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'd encourage the POPLMark authors to write a bunch of "use cases" for 
> some of the benchmarks. i.e. assuming they have their ideal mechanized 
> metatheory, what exactly would they do with it? Extract an executable 
> type-checker from the specification? Emit a witness to be certified by a 
> trusted verifier? Integrate the result into a larger verification 
> system?  Comparing a particular solution to a benchmark against a set of 
> fixed applications, I think would help focus and clarify the evaluation 
> process.

The benchmarks themselves are indended to serve as the kind of use-cases you
are asking for.  In particular, problem 3 is closely related to your
"Extract an executable type-checker from the specification."  We chose to
include this and exclude your other use-cases because this is the one that
we felt was the most important for our specific aim of "formalizing all (or
at least many) POPL papers."  

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.

Regards,

    - Benjamin