The Brown PLT Blog, 2012-06-04
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.
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.
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.
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.
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).
The examples are remarkable, check them out (but check the browser issues John discusses).
John has a little confession:
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...
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.