Lambda the Ultimate

ACM Press Release:

The ACM Special Interest Group on Programming Languages (SIGPLAN) today presents its first-ever Programming Languages Software Award to Chris Lattner of Apple Inc. for his design and development of the Low Level Virtual Machine (LLVM), a compiler infrastructure that has been quickly adopted by a wide array of industry and academic organizations. Since LLVM’s release as an open source compiler infrastructure in October 2003, companies including Apple, Adobe, and Cray have incorporated it into their commercial products, reflecting its simplicity, flexibility, and versatility.

Berp is an implementation of Python 3. At its heart is a translator, which takes Python code as input and generates Haskell code as output. The Haskell code is fed into a Haskell compiler (GHC) for compilation to machine code or interpretation as byte code.

This project sounds interesting. Has anyone checked it out?

David MacIver is doing a bit of a sociological study on how programmers pick The Right Tool for the job. Programmers select all the languages they know from a fairly mainstream and popular list and then rank those languages according to statements like "I find it easy to write efficient code in this language" and "When I write code in this language I can be very sure it is correct". At the end of the process the survey taker can see how languages ranked overall under each statement and what statements have been most strongly associated with each language.

Obviously this isn't a formal study and, as with all online surveys, there are going to be challenges with selection bias and with people trying to game the system. None-the-less, it is pretty interesting and fun as is. Perhaps something similar would be worth doing under more controlled circumstances (although it beats me how to feasibly get a large sample size of programmers without introducing selection bias).

This will probably interest many LtU readers:

Code Quarterly is a new publication [edited by Peter Seibel] that intends to publish in-depth articles of interest to hackers...

Here are some of the kinds of articles we hope to publish:

* Technical explanations – Pieces that explain a concept and why we should care...
* Code reads – guided tours through code that demonstrates interesting programming techniques or which is simply well-put-together, beautiful code.
* Q&A interviews – in-depth interviews with notable programmers.
* Think pieces – pieces about not-entirely-technical issues hackers would care about...
* Computer history – articles that take a look back at where our ideas about computers came from.
* Book reviews

If this sounds interesting and you can see yourself as either a a reader or a potential contributor hop over to the site and let them know.

The Structure of Authority: Why security is not a separable concern, by Mark S. Miller, Bill Tulloh, and Jonathan Shapiro:

Common programming practice grants excess authority for the sake of functionality; programming principles require least authority for the sake of security. If we practice our principles, we could have both security and functionality. Treating security as a separate concern has not succeeded in bridging the gap between principle and practice, because it operates without knowledge of what constitutes least authority. Only when requests are made -- whether by humans acting through a user interface, or by one object invoking another -- can we determine how much authority is adequate. Without this knowledge, we must provide programs with enough authority to do anything they might be requested to do.

We examine the practice of least authority at four major layers of abstraction -- from humans in an organization down to individual objects within a programming language. We explain the special role of object-capability languages -- such as E or the proposed Oz-E -- in supporting practical least authority.

An important overview of why security properties cannot be an after-thought for any platform, languages and operating systems included. To this end, the paper covers security properties at various granularities from desktop down to object-level granularity, and how object-capabilities provide security properties that are compositional, and permit safely composing mutually suspicious programs.

A recent LtU discussion on achieving security by built-in object-capabilities vs. building security frameworks as libraries reminded me of this paper. Ultimately, the library approach can work assuming side-effects are properly controlled via some mechanism, ie. effect types or monads, but any solution should conform to object capability principles to maintain safe composition.

An example of a capability-secure legacy/library approach is Plash (Principle of Least Authority SHell), which provides object-specific file system name spaces. Any library interface to the file system should mimic this file system virtualization, which effectively pushes side-effect control down to OS-level objects, and which is essential to safely composing mutually suspicious programs that access the file system.

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.

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.