[PRL] review of proposal

[Matthias Felleisen]

For the benefit of our junior members, I wrote a review that I would 
almost deliver to NSF for Mitch's proposal. You can hopefully tell 
where I use phrases that are inappropriate and where I left out 
explanations of detailed problems with the proposal. The format is 
almost completely what NSF demands. I left out a few ever-changing 
things. -- Matthias

MW, Foundational Studies in Programming

Summary: This proposal is really a combination of two separate, disjoint
  mini-proposals.

The first mini-proposal concerns proofs of observational equivalences. 
The
  problem is to prove that two phrases in a language are 
indistinguishable
  in all programs (context) in which they could occur. In the late 60s, 
70s,
  and 80s, people studied the theory of observational equivalence in a
  purely functional context. In the 80s, they turned their attention to
  imperative languages. Meyer (later with Sieber) showed in several 
papers
  how difficult it was to reason about observational equivalence in the
  presence of memory allocation and mutation (both in an Algol-like 
setting
  and in a higher-order setting).

The PI proposes to study a modification of the bisimulation approach to
  this problem. A bisimulation is a maximal-fixpoint approach to proving
  observational equivalences (adapted from concurrency to the sequential
  world). Through a rather technical looking change to the conventional
  definition, the relation can apparently deal with allocation and 
mutation
  in a surprisingly straightforward manner. The proposal claims (w/o 
proof)
  that the technique can cope with all of Meyer's puzzles.

The second mini-proposal concerns the study of syntactic abstraction 
(aka
  macros), specifically two different aspects: the notion of hygienic 
macros
  (now standard in Scheme) and macros for languages with old-fashioned,
  stupid syntax :-). With respect to hygiene, the proposal first explains
  the problem (but see below) and then indicates that the PI and his
  students have a new way of specifying hygiene as a variation of
  alpha-equivalence. With respect to macros for conventional syntax, the
  proposal is based on Cardelli et al.'s work on extensible languages. It
  explains why this is not syntactic abstraction, how to use it for macro
  abstraction, and why the resulting system should expand macros in a 
"lazy"
  rather than an "eager" fashion.

Evaluation:

A proposal should explain a problem, describe a solution approach in
  sufficient detail (or several approaches), and sketch a realistic 
path. It
  should also compare and contrast its approach with related attempts.

This proposal succeeds with this for the first mini-proposal but it 
fails
  almost completely in the second half.

Observational equivalence: The PI should have explained the topic and 
its
  relevance so that non-experts on this panel can understand it. Having 
said
  this, the proposal clearly forwards an idea on how to tackle this
  extremely difficult problem from a new angle. I am impressed by the 
kind
  of puzzles they can solve now. Earlier approaches based on operational
  semantics have succeeded in doing some of this, but the PI's approach
  appears to be powerful. -- The major problem I have with this part are 
the
  exaggerated claims that any of this may apply to OOP (possibly) or AOP
  (fantasy land).

I wish I understood how this compares to approaches based on 
denotational
  semantics (especially:

@article{ abramsky99full,
     author = "Samson Abramsky and Guy McCusker",
     title = "Full abstraction for {Idealized Algol} with passive 
expressions",
     journal = "Theoretical Computer Science",
     volume = "227",
     number = "1--2",
     pages = "3--42",
     year = "1999",
     url = "citeseer.ist.psu.edu/abramsky98full.html" }

and other new approaches based on games.)

Macros: The hygiene problem is explained reasonably well -- for people 
who
  like parentheses _and_ indentation, though I believe that "hygiene" is
  misrepresented in this proposal. (I personally transported the phrase 
from
  a Brandregt paper to the first hygiene paper. -- MF) The idea of using
  alpha equivalence to model this notion is obvious; almost everyone who
  studied the problem starting in 1986 had it. The plan sounds
  reasonable. What is missing is a new idea. If it is in there, I missed
  it. Completely.

  For the concrete syntax part, the PI and his students are taking a 
novel
  approach, using Cardelli et al.'s extensible language as a macro 
system. I
  wish they had included some examples so that I can understand how they 
did
  this. I don't even know whether they did it for BASIC or SML/NJ with
  higher-order functors. Given the writing, it is not obvious what they 
have
  accomplished, whether it's research or a cute hack. The discussion of 
lazy
  vs eager is entirely appropriate, though extremely abstract. Again, I 
wish
  they had explained this with examples. Worse, this part too entirely
  misses an explanation of how they intend to do better than the numerous
  failed approaches from the past, starting with Daniel Weise all the 
way to
  Maya.

Details:

The proposal feels "airy" that is, it wastes a lot of space. It repeats 
the
  summary inside the proposal, it doesn't use the full allotment of 
space. I
  would have liked to see the PI use the extra space to explain things in
  sufficient detail.

-- marked in the proposal -- 

Example: You mention macro systems as part of the module system but you
completely fail to discuss

How would your concrete syntax system deal with something like this:

(module foo mzscheme

   (m 10)

   (define-syntax m
     (syntax-rules ()
       [(_ x) (printf ">>> ~s~n" x)]))

   )

in your system?

--- more details ---

PI: The PI is well-known for delivering theoretical results for many 
years,
  and we can expect that he will do so in the future. According to the 
prior
  results section, he has also graduated three PhD students over the past
  five years.

Broad Impact: The proposal attempts to explain its impact on the 
context of
  PL research and CS but the prose is entirely boiler plate. So let's 
hope
  it will have some.