Re: [Scheme-reports] Formal Comment: clarify the semantics of the dynamic features

[Eli Barzilay <eli@x>]

Two hours ago, Jonathan Rees wrote:
> 
> On Jul 1, 2012, at 5:26 PM, Eli Barzilay wrote:
> 
> > 40 minutes ago, John Cowan wrote:
> >> 
> >> Form is content: the text of the draft is the only full expression
> >> of the semantics that exists.  If I had my druthers, the formal
> >> semantics would go away altogether, but then I'm prejudiced against
> >> formal semantics: see
> >> http://lambda-the-ultimate.org/node/4478#comment-69764 if you are
> >> interested in my views.
> > 
> > Coming from someone involved in designing a language, this would be a
> > pretty bad thing to say.  When applied to Scheme, it becomes
> > horrifyingly bad.
> > 
> > (Yes, this sounds like flaming, but I personally think that this is
> > *so* bad that it shouldn't go unhighlighted.)
> 
> John and I are here to horrify you!
> 
> You are just making a claim here.

To be specific about what horrifies me in this, it's the reflectively
bogus claim that:

  Since programming languages are already themselves formalisms

which might be true in some "the One implementation is the semantics"
languages, but that's not the case here.  (The rest of that
unfortunate blurb is misguided at best.)

In any case, that kind of statement is far from "the semantics section
of r*rs is unmotivated, non normative, and is both incomplete and
overdetermined" -- it's a rejection of the idea of *formal*
descriptions.  (Preferring to stick to a much weaker definition of
"formal".)


> Much as I love formalism, even when it's gratuitous, I have always
> felt uncomfortable with this particular denotational semantics. If
> the report said exactly *why* it's being provided that would
> help.

Then fix it instead of rejecting the idea of having a formal account.


> Is it supposed to convince the reader of consistency or some other
> formal property? (Denotational semanticses provide models and
> proving consistency is usually the reason one creates a model.) Is
> it supposed to help implementors? It does not seem to be normative,
> and it is both incomplete and overdetermined (it describes an
> "extended subset"), so its role is mysterious. I'm not saying it's
> bad or useless, just that the nature of its potential utility is not
> made clear by the report.

Yes, these are problems in the semantics part of r5rs, and much of
that was addressed in the r6rs semantics.  But for some reason, that
was all dumped, and instead the "new" text is the old one.  It's as if
nothing worthwile happened in the world of formalisms in the last few
decades.

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!