Lambda the Ultimate

A rather fun and instructive series of posts about implementing a cellular automaton in idiomatic Clojure, and making it run fast (and in parallel).

Be sure to read the second part, and the errata.

If the general idea wasn't enough to make you mad, or if you wrote it off as being purely an Apple/Adobe spat, this ought to cut a bit closer to LtU's heart...

Apple removes Scratch from iPad/iPhone/iTouch.

My wife has taught a couple of classes using Scratch with young kids, and to see the pride they feel at their creations is a marvelous thing. I think restricting their ability to share that feeling is really reprehensible. And the damage done to the programmers of tomorrow? Hard to say...

(Apologies for this being on the front page twice now, but I think this really deserves a post of its own...)

In seL4: Formal Verification of an Operating-System Kernel, Communications of the ACM, June, 2010 Klein et al

...report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code.

seL4 is a third-generation microkernel of L4 provenance, comprising 8,700 lines of C and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.

We prove that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as that the kernel will never crash, and it will never perform an unsafe operation. It also implies much more: we can predict precisely how the kernel will behave in every possible situation.

Overall the paper is more of an experience report than an in depth exploration of the kernel and its proofs but there is a some meat to be found. More information can be found at the sel4 website.

Maxine VM is an open source meta-circular JVM from Sun.

Maxine is a VM designed for and written in the Java(TM) Programming Language with an emphasis on leveraging meta-circularity, componentized design, and code reuse to achieve flexibility, configurability, and productivity for academic and industrial virtual machine researchers.

The Maxine Inspector [5min, YouTube] seems pretty neat! Bringing VM research to the masses :)
A longer presentation by Bernd Mathiske at the JVM Language Summit 2008 provides a good introduction.

The new iPhone developer agreement as quoted at http://daringfireball.net/2010/04/iphone_agreement_bans_flash_compiler:

3.3.1 — Applications may only use Documented APIs in the manner prescribed by Apple and must not use or call any private APIs. Applications must be originally written in Objective-C, C, C++, or JavaScript as executed by the iPhone OS WebKit engine, and only code written in C, C++, and Objective-C may compile and directly link against the Documented APIs (e.g., Applications that link to Documented APIs through an intermediary translation or compatibility layer or tool are prohibited).

Now think about this. Basically, they have said "you can only use these PLs to originally write your code, use of any other PLs breaks this agreement." Now, assume iPhone continues to be widely successful and that...eventually PCs are replaced by iPad devices. And say everyone starts copying Apple's locked fortress model, where will PL innovation go?

I'm very disappointed at Apple over this.

This might be of interest to people that will be at OSCON 2010 or will be in Portland, Oregon on July 21-22.

Announcing the First Emerging Languages Conference

As new problems in computing arise, new languages are being created to help tackle those problems. We’re proud to announce an event that brings together programming language creators, implementors, researchers, and enthusiasts to share their creations, experiences, and challenges. Our goal for the event is nothing less than advancing the state of the art in programming language design and implementation.

Initial list of speakers include designers for Go, Io, Duby, Kodu, Newspeak, CoffeeScript, Ur, Objective-J, BitC and F#.

A Formal System For Euclid's Elements, Jeremy Avigad, Edward Dean, and John Mumma. Review of Symbolic Logic, Vol. 2, No. 4, 2009.

Abstract. We present a formal system, E, which provides a faithful model of the proofs in Euclid’s Elements, including the use of diagrammatic reasoning.

Diagrammatic languages are a perennial favorite discussion topic here, and Euclid's proofs constitute one of the oldest diagrammatic languages around. And yet for hundreds of years (at least since Leibniz) people have argued about whether or not the diagrams are really part of a formal system of reasoning, or whether they are simply visual aids hanging on the side of the true proof. The latter position is the one that Hilbert and Tarski took as well when they gave formal axiomatic systems for geometry.

But was this necessary, or just a contingent fact of the logical machinery available to them? Avigad and his coauthors show the former point of view also works, and that you can do it with very basic proof theory (there's little here unfamiliar to anyone who has read Pierce's book). Yet it sheds a lot of light on how the diagrams in the Elements work, in part because of their very careful analysis of how to read the diagrams -- that is, what conclusion a diagram really licenses you to draw, and which ones are accidents of the specific figure on the page. How they consider these issues is a good model for anyone designing their own visual programming languages.

Roberto Ierusalimschy discusses the ideas behind the design of Lua specially on the pervasive use of tables and coroutines.

Video, Slides[PDF] and Talk Abstract.

Note: The video is in Windows Media format but it works with Quicktime Player on the Mac if you have Flip4Mac WMV installed. I can open the video using File->Open URL.

Conal Elliott's weblog post from January, Can functional programming be liberated from the von Neumann paradigm?, makes the case that the kind of coupling to state which Haskell programs making use of the IO monad have, raise problems of the same sort that led to pure functional programming in the first place. Conal then goes on to sketch, with reference to his work on FRP and denotational design, some ideas about where purity should be leading language design.

A nice blog post about "little mini-languages" that form part of the syntax of Clojure.