Mechanized LambdaJS | Hacker News Reader

Mechanized LambdaJS

brownplt.github.com

30 pointsllambda12 comments

This is really interesting. I'm quite curious what they've left out of their reduced subset of javascript, but unfortunately I don't have the time to dig in right now.

Has anyone else taken a tour through their codebase?

Actually, what the hell, I'll download haskell, run their interpreter, and see about getting the underscore.js test suite to run.

It's not so much a reduced subset as a kernel language: the full ECMAScript Edition 5 language can be translated down to the kernel language, so in principle they can actually model the behavior of any program that the language defined by the standard admits.

There have been a few attempts to formalize the semantics of JS, but the lambdaJS approach is the most practical: by factoring out the incidental details (the "syntactic sugar") as a translation ("desugaring") to a kernel language, any work you do on the formal semantics of the language only has to focus on the smaller kernel.

This is also a really practical way to approach building tools for JS, like static analysis: if you design a single desugaring pass as a translation, then you can build a whole bunch of tools on the kernel language. Same idea roughly as the standard compilers approach of translating to an IR.

Sure, I took it to be akin to the way that coffeescript maps down to JS, they're mapping JS down to LambdaJS.

But that said, having read through their blog posts, I was under the impression that their interpreter doesn't in fact support all of the SpiderMonkey test suite, and so, as a practical matter is still only supporting a subset of JS.

My attempts to get underscore working have been unsuccessful thus far (the debug info isn't terribly useful, not knowing their codebase).

It looks like the λJS has an issue parsing some of the escape sequences in underscore.js; it's a bug in WebBits parser that version uses.

Another implementation of the core semantics + desugaring approach, dubbed S5 (https://github.com/brownplt/lambdas5), is better engineered and actually uses SpiderMonkey's parser to handle more programs.

S5 runs underscore.js without any issues. Do give it a shot if you're still interested in trying things out.

Also, it's worth mentioning that S5 handles features of the new ECMAScript 5 specification, like strict mode, getters and setters, and new APIs, that the original λJS simply doesn't handle, so it's a much more complete account of JavaScript.

Thanks for the info :)

I lament that HN has lost its way enough that this thread didn't make it anywhere near the top of the homepage.

That's at least partly because SpiderMonkey supports a superset of the ES5 language, including Mozilla-specific extensions and candidate features for future versions of the standard.

Dave

It's amazing how similar Javascript and Lua are. For example, the following three statements are equivalent:

    > JS:   { x : 2 + 3, y : 9 }["x"]  * (11 + 23)
    > Lua: ({ x = 2 + 3, y = 9 })["x"] * (11 + 23)
    > Lua: ({ x = 2 + 3, y = 9 }).x    * (11 + 23)

this seems hilarious before my morning cup of coffee and before getting ready to dive into a real world Js project :) : "We say "agreed" and not "passed" because SpiderMonkey fails some of its own tests. Without any other standard of correctness, λJS strives for bug-compatibility with SpiderMonkey on those tests."

This looks really interesting but I don't have the background to understand it. What is going on here?

λJS is a mathematically formalized version of (a subset of) JavaScript. It is not like a traditional mathematical definition (computer scientists often use a tool named "operational semantics" to greatly simplify this stuff) but nevertheless can be analyzed as like a mathematical one. To the extent that they claimed to prove the soundness, i.e. any well-formed program which λJS thinks to be valid should not go other ways that λJS does not allow. This forms a basic premise that can be used to analyze λJS program (and hopefully, actual JavaScript program).

Of course, this holds when λJS is really correct and a good model for JavaScript. Unfortunately they have found that there is a severe hole left in λJS after they had a (now wrong) correctness theorem. In light of this problem, they now mechanically proved that there are no more holes left in λJS. Unlike a hand-written proof a mechanized proof can be verified by a relatively simple[1] program, so you don't need to believe yourself but just the program. As mechanized proofs need to describe every detail, this is not a simple task, and that's what they did.

[1] A lot simpler than the actual human.

Thanks for the attempt to explain. However, it's slightly off on several fronts, so I'd like to set the record straight.

I don't know what you mean when you say it's not a "traditional mathematical definition". It's both traditional and mathematical enough.

An "operational semantics" is not necessarily a simplification. Whether or not it's a simplification is a function of what you are specifying.

We chose a route whereby a compiler reduces all of JS to a simpler language (λJS) and then provided an operational semantics for that simpler language. Neither is this non-mathematical nor is the simplification inherent to an operational semantics.

Your restatement of soundness contains dangerous words that have other, technical meanings (like "valid") and is also not quite right. The soundness being proven here is called "untyped soundness", and it simply means "the semantics didn't forget any cases that should have been defined". Perhaps that is what you meant to say, but I'd suggest this way of saying it is a lot less obscure.

Our previous formulation missed a few cases. The cases were sufficiently obscure that all our prior testing and use did not catch them. So I'd say this hardly warrants the label "severe". You can see the sum total of change here (the link was in the original post):

https://github.com/brownplt/LambdaJS/commit/9a7e67ab896c8db3...

Also, our previous attempt to confirm untyped soundness was not hand-written. It too was mechanical, but it used a state-exploration strategy. This caught lots of problems, which we fixed, but because it could not explore the state exhaustively, it missed a few that we hadn't noticed. The strategy in this post explores the state exhaustively (through a proof-assistant).

Hope that clarifies.

Thank you for the clarification. I've certainly oversimplified things too much, as my explanation was intended for layman (for example, I did not bother about the technical meaning of "valid" and "correct"). The word "traditional" meant that most people without PL knowledge would not have seen that (albeit the structural definition is far more basic than many other kinds of definitions). In the other hands, I forgot that the claim described in Section 3 of the ECOOP paper does not use a hand-written proof---I think the paper utilizes a handful number of other hand-written proofs, however.

Having tried to augment and test λJS myself, I'm very glad to hear that it is now fully mechanized. Keep up good work, :-)

Reply on news.ycombinator.com