4 ms·

Mechanized LambdaJS

30 points by llambda 14y ago

positr0n 14y ago
This looks really interesting but I don't have the background to understand it. What is going on here?
- lifthrasiir 14y ago
  λ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.
  - shriramkmurthi 14y ago
    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/9a7e67ab896c8db3f12cdfe3aa6fe74e192b1b00 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.
    - lifthrasiir 14y ago
      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, :-)
nnq 14y ago
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."
knowtheory 14y ago
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.
- dherman 14y ago
  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.
  - knowtheory 14y ago
    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).
    - dherman 14y ago
      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
ncarlson 14y ago
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)

Mechanized LambdaJS

30 points by llambda 14y ago

positr0n 14y ago

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

lifthrasiir 14y ago
λ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.
- shriramkmurthi 14y ago
  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/9a7e67ab896c8db3f12cdfe3aa6fe74e192b1b00 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.
  - lifthrasiir 14y ago
    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, :-)

nnq 14y ago

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."

knowtheory 14y ago

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.

dherman 14y ago
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.
- knowtheory 14y ago
  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).
  - dherman 14y ago
    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

ncarlson 14y ago

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)