Re: JSCert: a JavaScript formalisation in the Coq theorem prover

Thanks :) G Quildreen Motta writes: > Ah, this looks really neat! :D > > I wasn't familiar with any research on formalising JavaScript semantics > besides λjs, so it's neat to see more research on this front :) > > > On 25 January 2014 22:55, Gareth Smith wrote: > >> >> Apologies if this is a

Re: JSCert: a JavaScript formalisation in the Coq theorem prover

Ah, this looks really neat! :D I wasn't familiar with any research on formalising JavaScript semantics besides λjs, so it's neat to see more research on this front :) On 25 January 2014 22:55, Gareth Smith wrote: > > Apologies if this is a duplicate - I tried sending this earlier, but it > did

JSCert: a JavaScript formalisation in the Coq theorem prover

Apologies if this is a duplicate - I tried sending this earlier, but it didn't seem to go through. Gareth Smith writes: > We are pleased to announce JSCert, a formalisation of Chapters 8-14 of > the ES5 standard. > > We've built JSCert using the Coq proof assistant, using the same > metaphors

Re: detecting JS language mode for tools

John Barton wrote: The Script goal disallows 'import' and 'export' specifically to ensure that the Script goal is inconvenient for developers and thus they are encouraged to shift to the Module goal. No, that's not the rationale. The reason is to avoid enabling more synchronous

Re: detecting JS language mode for tools

Peter van der Zee wrote: `` Again, no two-way fallback option. Clever thought re: implicit CDATA content model, though! /be ___ es-discuss mailing list es-discuss@mozilla.org https://mail.mozilla.org/listinfo/es-discuss

Re: detecting JS language mode for tools

David Sheets wrote: . Old browsers ignore the new attribute will process the content, which > could be written to work "both ways". Is a new attribute necessary? What about using @type? Old browsers will ignore unknown types, losing the two-way fallback option. /be _

Re: Fwd: Reason why generators do not have references to themselves?

[replying to a message you sent off-list, hope it is ok. /be] Brendan Eich wrote: Bradley Meck wrote: Perhaps, but I am still a bit concerned functionality wise that I do not have a clean way to force the `new generator()` piece of code to be inside of the generator. I think you've gone down

Re: detecting JS language mode for tools

Well, sorry my extra angle brackets. Let me try again. Allen says, if I understand correctly, that the tiresome complexity of the second parsing goal will be repaid when the superior Module goal supplants the Script goal. But we undermine this tradeoff by allowing Scripts to use System and Loader.

Re: transpiling ES6 generator functions to ES5: what next?

My experience implementing Regenerator is consistent with the nuance that Brendan is highlighting here, as I understand it. The state machines that Regenerator produces behave to the outside world almost exactly as generators are supposed to behave, but there are gaps: as an example, direct eval i

Re: detecting JS language mode for tools

`` "It's not a script, it's a module!" On Sat, Jan 25, 2014 at 3:34 PM, David Sheets wrote: > On Sat, Jan 25, 2014 at 2:33 AM, Brendan Eich wrote: >> John Barton wrote: >> >>> On Fri, Jan 24, 2014 at 12:17 PM, Allen Wirfs-Brock >> > wrote: >>> >>> I should have

Re: detecting JS language mode for tools

On Sat, Jan 25, 2014 at 2:33 AM, Brendan Eich wrote: > John Barton wrote: > >> On Fri, Jan 24, 2014 at 12:17 PM, Allen Wirfs-Brock > > wrote: >> >> I should have also included: >> >> 2A) Hopefully, overtime, the old script syntactic goal will fade >> from

Re: Reason why generators do not have references to themselves?

Le 24 janv. 2014 à 10:06, Bradley Meck a écrit : > (...) I still have to use new when invoking the generator function which > feels dirty in my mind. Interestingly, using `new` when invoking a generator function feels cleaner in my mind. :-) In short (and since it is somewhat off-topic), `new