Specification styles

Forrest L Norvell forrest at newrelic.com
Thu Jan 30 11:52:40 PST 2014


On Thu, Jan 30, 2014 at 11:07 AM, Boris Zbarsky <bzbarsky at mit.edu> wrote:

> On 1/30/14 10:20 AM, Forrest L Norvell wrote:
>
>> So far, this has been a very straightforward spec to implement.
>>
>
> Forrest,
>
> I think I may have been a bit unclear, my apologies.
>
> I think we all agree that ES-style specifications are in fact more
> straightforward to transcribe into an ES implementation.
>
> What is harder, in my experience, is understanding whether the
> specification actually says what it means to say and determining whether
> there are bugs in the specification.  This arises to some extent from the
> core functionality being partially obscured by a fair amount of boilerplate.
>

I agree with this entirely, with the caveat that "partially obscured" and
even "boilerplate" are in this case subjective factors. Once you split
Domenic's streams documentation into two pieces -- a narrative, informal
piece explaining the design and its motivation, and the specification
proper, which is still informal but more organized -- the specification
itself seems neither particularly verbose nor overdetermined. Again, this
is my subjective interpretation, but I've spent a fair amount of time
dealing with specifications (and, just to be clear, mostly not in the
JavaScript world).

Neither WebIDL nor the style of ES-262 are formal specification languages,
nor do they specify any kind of rigorous operational semantics. This isn't
a problem, as that's not their purpose. Their purpose, as I understand it,
is to facilitate the specification of behavior in such a way that a
consensus can be formed as to whether a given implementation is congruent
with a given design (and, more nebulously, the designers' intent).

Now I agree this is somewhat subjective.  Some people prefer to have all
> the complications explicitly written out, both in specifications and in
> code, while others prefer reusable tested black boxes that have certain
> defined behavior.  The former approach is much more verbose and can thus
> hinder understanding of the big picture.  The latter approach involves
> in-depth understanding of the black boxes to understand the details.  In
> practice, both the WebIDL and ES styles use some mixture of the two; what
> differs is the exact set of black boxes used.  The ES style black boxes are
> mostly more fine-grained than the WebIDL ones.
>

I agree with this description, and I wish there were a way to support both
approaches. Neither the declarative style of WebIDL nor the imperative
style of ES-262 are good at capturing both at the same time. As designers
and researchers we want to be able to point to the formal model and, if not
prove, at least attempt to make strong assertions about particular
behaviors or abstractions. As implementors, it's much easier to work from
imperative descriptions of behavior, and the process of resolving the
ambiguities during implementation will surface aspects of the design that
are not obvious when looking at a declarative model.

I spoke up in this thread because my primary purpose in taking on the
effort of implementing Domenic's spec was to figure out how I feel about it
(spoiler: so far I feel pretty good!). The easiest way for me to get up to
speed was to write some code (and tests) to see what gotchas popped up in
the real world (as streams have historically been probably the most fertile
source of edge cases in Node). For this purpose, Domenic's choice of
specification style has been ideal, for me.


> I wish I had a good way to combine the strengths of the two approaches
> more than existing specification formalisms do right now.  In some ways,
> something that allows looking at higher-level definition in terms of black
> boxes and then on-demand (e.g. a "expand this" or "expand all in this
> section" link) allows the reader to inline the black boxes to see all the
> details might be a possibility.  That would involve creating some tooling,
> obviously.


I think the underlying problem is that neither of these are truly formal,
at least not in the sense that I understand it. There's structure and some
essays at rigor, but nothing like, say, the recent implementation of ES5 in
Coq (which is awesome) or a Robert Harper-style operational semantics
rooted in axiomatic logic. On the other hand, I don't think formalism is
really what WebIDL is after.

As an implementor, I find this all a refreshing contrast to trying to
>> wrap my head around WebIDL
>>
>
> I honestly think that this (just like other people's experiences with
> trying to wrap their heads around ECMASpeak) is at least partially due to
> familiarity, or lack thereof, with the black boxes being used as
> specification primitives...  Partially it may be due to the wrong
> primitives being used, of course, which is a real problem in both styles I
> believe.


I'm fine with black boxes, and referring to standards documents when
decrypting specifications (I've had to work with ASN.1, I did a fair amount
of CORBA development with its IDL once upon a time, etc). I just find the
level of abstraction chosen for WebIDL inappropriate for JavaScript. For
example, WebIDL's pretense that there are multiple numeric types in the web
platform, when in fact there is only a relatively narrow domain
(TypedArrays, browser / DOM objects that aren't hosted in JavaScript, etc)
where that kind of typing is applicable.

I understand that tradeoffs are necessary to support specifications that
cross such a wide domain of use cases and implementation technologies, but
WebIDL just feels at odds with the way I understand the web platform to
work. It's a very imprecise mapping, I guess is how I feel.

I have nothing against formal specification methods per se, but, at least
>> for things
>> that are implementable in pure JavaScript (as Domenic's proposal is)
>>
>
> It's not, actually, since it requires asynchronous callbacks which do not
> currently exist in pure JavaScript.  This is not quite a nitpick, since
> properly defining asynchronous callbacks is a fairly nontrivial matter with
> security implications, as I already pointed out in this thread.


It's interesting that you raise this issue, because all of the aspects
involving asynchronicity and callbacks in Domenic's spec do so in the
context of ES promises, and unless I'm missing something, all of the
trickiness around it is handled by the promises specification, leaving the
streams proposal as a simple consumer of that spec. Am I missing something?

F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20140130/2f72da31/attachment.html>


More information about the es-discuss mailing list