Re: Fusion Laws?

On Thursday, March 31, 2016 at 1:22:14 PM UTC-5, Jason Orendorff wrote:
> On Wed, Mar 30, 2016 at 10:32 PM, Michael Haufe wrote:
> 
> > It's a shame there isn't an Attribute Grammar definition for the semantics
> > of ECMAScript, it might make this a bit more tractable...
> >
> 
> Believe it or not, the specification itself is all attribute grammars,
> including the parts that define Evaluation. It's not written in a real
> formal language, and it's a weird mash-up of declarative and procedural
> style, but it's close enough to attribute grammars that you can see exactly
> how you would go about formalizing it.

Yes, the formal language was what I was referring to. It's a fair point. My off-side comment was more towards being able to poke at those semantics as easily as one might poke at a BNF grammar and see what goes wrong when it's run through a verifier (like specifying isTailPosition or isPure from earlier in the thread).

> The specification technique isn't the problem. It's the semantics being
> specified. They are the semantics of a dynamic language. Reasoning about
> such code is an exercise in hand-waving.

Perhaps I'm misreading your statement here, but are you saying that the current spec is hand-waving the runtime semantics of the language, or are you instead saying that one can't formalize the semantics of a dynamic language?