[POPLmark] Meta-comment

[Daniel C. Wang]

Greg Morrisett wrote:

> {stuff deleted}
> -Greg
> p.s. Most fun reading I've had in a while...

Indeed.... I'd like to make a hopefully constructive meta-comment about 
the structure of the POPLMark and the various HOAS issues in general. I 
personally find the POPLMark's goals a bit under specified. The two 
questions outlined in the challenge are

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

For example lets consider the issue of closure conversion and 
HOAS/HOAJ.  If the application of the formalized metatheory is to be 
used in a PCC//TAL scenario the lack of an obvious way for HOAS/HOAJ and 
closure-conversion to co-exists is a moot point, and the benefits of 
HOAS are a big win or a wash depending on how much binding you have to 
deal with. However, if one were interested in doing translation 
validation HOAS/HOAJ is most likely a non-starter.

In general, I think many of the objections to HOAS have been presented 
in a "but what if.. I want to do X" fashion. I think unless there is 
some more concrete guidence about the sets of uses for the metatheory 
are given, one can always raise some hypothetical issue for any system 
and complain.

Karl brought up an interesting point about the trade off between 
possibility and feasibility. This is indeed a very delicate trade off. 
Each system makes a different set of choices for different sets of 
features.

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.

I personally find it a bit irrksome that one of the biggest application 
for mechnaized-metatheory (FPCC/PCC/TALS) are not specificly mentioned 
in the challenge. In the past I've not complained because, I thought the 
POPLMark authors had some more general goals/applications in mind, but 
now I feel like the POPLMarks goals are general too the point of being 
"too fuzzy" for submitters to know what is actually on the minds of the 
POPLMark author's mind.



Unfortunately, I think the POPLMark as I currently understand it has 
devolved into a "binding micro-benchmark", and doesn't capature as wide 
a scope of problems as I think the authors intended.