Lambda the Ultimate

Mechanized λ_JS
The Brown PLT Blog, 2012-06-04

In an earlier post, we introduced λ_JS, our operational semantics for JavaScript. Unlike many other operational semantics, λ_JS is no toy, but strives to correctly model JavaScript's messy details. To validate these claims, we test λ_JS with randomly generated tests and with portions of the Mozilla JavaScript test suite.

Testing is not enough. Despite our work, other researchers found a missing case in λ_JS. Today, we're introducing Mechanized λ_JS, which comes with a machine-checked proof of correctness, using the Coq proof assistant.

More work on mechanizing the actual, implemented semantics of a real language, rather than a toy.

Interactive Tutorial of the Sequent Calculus by Edward Z. Yang.

This interactive tutorial will teach you how to use the sequent calculus, a simple set of rules with which you can use to show the truth of statements in first order logic. It is geared towards anyone with some background in writing software for computers, with knowledge of basic boolean logic. ...

Proving theorems is not for the mathematicians anymore: with theorem provers, it's now a job for the hacker. — Martin Rinard ...

A common complaint with a formal systems like the sequent calculus is the "I clicked around and managed to prove this, but I'm not really sure what happened!" This is what Martin means by the hacker mentality: it is now possible for people to prove things, even when they don't know what they're doing. The computer will ensure that, in the end, they will have gotten it right.

The tool behind this nice tutorial is Logitext.

Note: Saw this on Sunday (9/11), but waited for it to go viral before posting it here.

A leaked Google memo, The Future of JavaScript, from November 2010 is being circulated around the Internet, outlining Google's supposed technical strategy for Web programming languages. Google plans to improve JavaScript, while also creating a competitor to JavaScript, Dart (ex-Dash), that it hopes will be the new lingua franca of the Web.

Ironically, I saw this leak via a Google Alert keyword search. It has propagated to at least Github, the Dzone social network, The Register and Information Week since Sunday.

Google Web Toolkit, which compiles Java to JavaScript for running code in the browser, now includes Code Splitting, for reducing application download time:

To split your code, simply insert calls to the method GWT.runAsync at the places where you want the program to be able to pause for downloading more code. These locations are called split points.

A call to GWT.runAsync is just like a call to register any other event handler. The only difference is that the event being handled is somewhat unusual. Instead of being a mouse-click event or key-press event, the event is that the necessary code has downloaded for execution to proceed.

In very disappointing news proper tail calls are out of ES4. It seems that a justification for tail calls could not be found. For example, here is Adobe's position on tail calls:

A more serious point is that we can't avoid adding tail calls at some point if we cater to the functional programming crowd. However, if we really intend to cater to them then we need to provide data structures that are functional too, like lists and operations on them—unlike ES arrays, which are entirely imperative. Of course users can implement those data structures themselves, if they have tail calls, but right now just adding tail calls “for functional programming” seems like a half solution.

Finally, tail calls preclude the use of straightforward implementation techniques for procedure calls. To be sure they are less limiting than generators, as one-shot continuations or longjumps are sufficient to handle tail calls in a non-tail-calling implementation language, but implementations that want good-performance tail calls must necessarily switch to a code generation technique.

This seems misguided. The user can implement functional data structures but not tail calls (without whole program transformation), so the later are much more valuable than the former. Furthermore, as a functional programmer I'm quite happy to use mutable data structures but I would certainly miss tail calls. Finally, every JS implementation is already shifting to code generation because straightforward implementation techniques are too slow for the existing idioms used in JS code.

The ES4 Wiki still indicates that tail calls are in, so perhaps they'll yet make it. For laughs you might want to look at the Ecmascript progress spreadsheet. Apple sure don't like change.

You can read the docs and download the C++ source here.

V8 is supposedly the main added value of Chrome, the newly announced Google browser.

Our discussion of the Chrome announcement enumerates some of the features of V8.

I guess we should note the attempts to smooth over the split amongst implementers that is going down in the JavaScript community with the Oslo Summit and Harmony trying to bring back peace. All programming languages are politics. The attempt to do the right things runs into competing interests and debates over what is the right thing to do. The split in the JavaScript community has been apparent now for a while, with the incrementalists wrapped up in version 3.1 and the more ambitious wrapped up in 4.0. Here's hoping that the wheels don't fall off. From a programming language standpoint, the particulars aren't as interesting as observing how language evolution takes place.

TileStack is an attempt to resurrect HyperCard and bring it to the web.

Running online there are going to be limitations about which stacks can be ported, which may reduce the usefulness and impact of this project, but maybe a standalone version will come later.

The system compiles Speak (the TileStack version of HyperTalk) to Javascript. If the result is not obfuscated, something I haven't verified, it may be possible to augment the output from TileStack with additional capabilities not supported or not yet implemented.

From the compatibility angle it is interesting to note that they renamed the language and seem to imply they are going to extend it beyond HyperTalk, without giving any specific guarantee about future compatibility. I'd suggest releasing the compiler that's as close to full HyperTalk compatibility as a separate product (or even, if they can bring themselves to do it, releasing it as open source).

John Resig (of jQuery fame) has ported the Processing visualization language to JavaScript.

The examples are remarkable, check them out (but check the browser issues John discusses).

John has a little confession:

The first portion of the project was writing a parser to dynamically convert code written in the Processing language, to JavaScript. This involves a lot of gnarly regular expressions chewing up the code, spitting it out in a format that the browser understands.

It works "fairly well" (in that it's able to handle anything that the processing.org web site throws at it) but I'm sure its total scope is limited (until a proper parser is involved). I felt bad about tackling this using regular expressions until I found out that the original Processing code base did it in the same manner (they now use a real parser, naturally).

Actually that's quite cool in itself (even if angels weep at this parsing code, I think we on LtU shouldn't cast the first stone). DSLs should be easily built and played with. Cleaning up the implementation comes later, if at all.

Purists may not only object to the regular expression parsing, but also to the central line of code which ties things together, namely: eval(parse(code, p)). But then, DSL lovers are not the sort of people to object to eval...

In the old days of LtU we regularly posted links to cool small interpreters that people could play with. Some of the more amusing ones were javascript based, and the page contained a REPL form (Luke, I am talking to you!). It is a shame we don't post more stuff like this, in between the more highbrow discussions...

Evolutionary Programming and Gradual Typing in ECMAScript 4, by Lars T Hansen, Adobe Systems, is an 18 page tutorial detailing features of ECMAScript 4, and how they can be applied to existing ECMAScript code to improve it.

This tutorial uses a simple library as a running example to illustrate the evolution of a program from the ES3 "script" stage, via various levels of typing and rigor, to an ES4 package with greater guarantees of integrity and better performance potential than the original code. We then look at how union types, generic functions, and reflection can be used to work with a library whose code we can't modify.