Lambda the Ultimate

Google open sources Szl - compiler and runtime for Sawzall Language:

Sawzall is a procedural language developed for parallel analysis of very large data sets (such as logs). It provides protocol buffer handling, regular expression support, string and array manipulation, associative arrays (maps), structured data (tuples), data fingerprinting (64-bit hash values), time values, various utility operations and the usual library functions operating on floating-point and string values. For years Sawzall has been Google's logs processing language of choice and is used for various other data analysis tasks across the company.

The original paper from Rob Pike et al.

Several years ago, a reading group I was in read about the Flux OSKit Project, which aimed to provide a modular basis for operating systems. One of the topics of discussion was the possibility of, and possible benefits of, an application-specific OS. (For example, the fearful spectre of EmacsOS was raised.)

Today, I ran across "Turning down the LAMP: Software specialization for the cloud", which actually makes a pretty strong case for the idea on a virtual machine infrastructure,

...We instead view the cloud as a stable hardware platform, and present a programming framework which permits applications to be constructed to run directly on top of it without intervening software layers. Our prototype (dubbed Mirage) is unashamedly academic; it extends the Objective Caml language with storage extensions and a custom run-time to emit binaries that execute as a guest operating system under Xen. Mirage applications exhibit significant performance speedups for I/O and memory handling versus the same code running under Linux/Xen.

As one example,

Frameworks which currently use (for example) fork(2) on a host to spawn processes would benefit from using cloud management APIs to request resources and eliminate the distinction between cores and hosts.

On the other hand, I suspect that this "unashamedly academic" idea may already be advancing into the commercial arena, if I am correctly reading between the lines of the VMware vFabric tc Server^TM marketing material.

Robert DeLine, Gina Venolia, and Kael Rowan, "Software Development with Code Maps", Communications of the ACM, Vol. 53 No. 8, Pages 48-54, 10.1145/1787234.1787250

Getting lost in a large code base is altogether too easy. The code consists of many thousands of symbols, with few visual landmarks to guide the eye. As a developer navigates the code, she follows hyperlinks, such as jumping from a method caller to a callee, with no visual transition to show where the jump landed. ... Better support for code diagrams in the development environment could support code understanding and communication, and could serve as a "map" to help keep developers oriented. ... Our goal is to integrate maps into the development environment such that developers can carry out most tasks within the map.

Although the focus of this article is largely on "Code Map as UI", there are hints of the possibility that we might eventually see "Code Map as Language Element" (for example, the comment that "An important lesson from the Oahu research is that developers assign meaning to the spatial layout of the code. Code Canvas therefore takes a mixed initiative approach to layout. The user is able to place any box on the map through direct manipulation..."). The same ideas will of course be familiar to anyone who has worked with environments like Simulink, which provide a combination of diagrammatic structuring and textual definition of algorithms. But in the past such environments have only really been found in specific application domains -- control systems and signal processing in the case of Simulink -- while the Code Map idea seems targeted at more general-purpose software development. Is the complexity of large software systems pushing us towards a situation in which graphical structures like Code Maps will become a common part of the syntax of general-purpose programming languages?

Fortifying Macros. Ryan Culpepper, Matthias Felleisen, ICFP 2010.

Existing macro systems force programmers to make a choice between clarity of specification and robustness. If they choose clarity, they must forgo validating significant parts of the specification and thus produce low-quality language extensions. If they choose robustness, they must write in a style that mingles the implementation with the specification and therefore obscures the latter. This paper introduces a new language for writing macros. With the new macro system, programmers naturally write robust language extensions using easy-to-understand specifications. The system translates these specifications into validators that detect misuses—including violations of context-sensitive constraints—and automatically synthesize appropriate feedback, eliminating the need for ad hoc validation code.

Presents syntax-parse, which seems like a truly great advancement over existing macro writing facilities.

Scribble: Closing the Book on Ad Hoc Documentation Tools. Matthew Flatt, Eli Barzilay, and Robert Bruce Findler. ICFP '09.

Scribble is a new system for writing library documentation, user guides, and tutorials. Scribble builds on PLT Scheme’s technology for language extension, and at its heart is a new approach to connecting prose references with library bindings. We have built Scribble libraries that support standalone documentation and papers, JavaDoc-style API documentation, and literate programming. Thanks in large part to Scribble’s flexibility and the ease with which we can cross-reference information across different levels, the documentation that is distributed with PLT Scheme now runs into the thousands of pages. This paper reports on the use of Scribble and on its design as both an extension and extensible part of PLT Scheme.

This introduces a cute and well thought out syntax for writing technical prose and for escaping back into the PL for typesetting operations and cross-references to PL values. It looks reminiscent of TeX, but has a direct transformation to S-expressions. Scribble also makes great use of PLT Scheme's modular and polyglot programming facilities.

A nice twist on the classic Scheme ploy:

A documentation language should be designed not by piling escape conventions on top of a comment syntax, but by removing the weaknesses and restrictions of the programming language that make a separate documentation language appear necessary. Scribble demonstrates that a small number of rules for forming documentation, with no restrictions on how they are composed, suffice to form a practical and efficient documentation language that is flexible enough to support the major documentation paradigms in use today.

(P.S. To which I'd like to add, somewhat OT, that compared to PLT Scheme, Common Lisp is starting to look teeny.)

The introduction of Helios (Eclipse 3.6) included the release of version 1.0 of Xtext - Language Development Framework.

With Xtext you can easily create your own programming languages and domain-specific languages (DSLs). The framework supports the development of language infrastructures including compilers and interpreters as well as full blown Eclipse-based IDE integration.

Given a grammar, Xtext derives a parser and an IDE with syntax highlighting, code completion, code folding, outline view, real-time error reporting, quick fixes among other standard IDE features. The models then can be used as an EMF Resource(ie as an interpreter) or with a little more work they can be used to generate code as well.

Check out the video clips on their website or the Webinar for a more detailed look.

OpenSCAD is a software for creating solid 3D CAD objects... OpenSCAD is not an interactive modeller. Instead it is something like a 3D-compiler that reads in a script file that describes the object and renders the 3D model from this script file (see examples below). This gives you (the designer) full control over the modelling process and enables you to easily change any step in the modelling process or make designes that are defined by configurable parameters.

In days gone by I used to post examples demonstrating the power of DSLs over GUIs. This is a nice example I came across recently. The scripting approach may be useful, of course, to 2D CAD as well. Here is an amusing example.

Maybe the analog computing DSL I fantasized about should output SCAD scripts instead of compiling directly to g-code...

Milawa: A Self-Verifying Theorem Prover for an ACL2-Like Logic

Milawa is a "self-verifying" theorem prover for an ACL2-like logic.

We begin with a simple proof checker, call it A, which is short enough to verify by the "social process" of mathematics.

We then develop a series of increasingly powerful proof checkers, call them B, C, D, and so on. We show that each of these is sound: they accept only the same formulas as A. We use A to verify B, and B to verify C, and so on. Then, since we trust A, and A says B is sound, we can trust B, and so on for C, D, and the rest.

Our final proof checker is really a theorem prover; it can carry out a goal-directed proof search using assumptions, calculation, rewrite rules, and so on. We use this theorem prover to discover the proofs of soundness for B, C, and so on, and to emit these proofs in a format that A can check. Hence, "self verifying."

This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview.

While I like the general idea, it seems this project didn't go far enough.

What I think would be cool is to develop are DSLs that compile to g-code. For example, putting my hacker hat on, I think it might be fun to build a DSL for describing mechanical (analog) computers, this will compile into g-code for cams, shafts, gears etc. that could then be manufactured using CNC machines and/or 3D printers...

The Monad Zipper by Bruno Oliveira and Tom Schrijvers

Limitations of monad stacks get in the way of developing highly
modular programs with effects. This pearl demonstrates that Functional
Programming’s abstraction tools are up to the challenge. Of
course, abstraction must be followed by clever instantiation: Huet’s
zipper for the monad stack makes components jump through unanticipated
hoops.

The monad zipper gives us new ways to compose monadic code operating with different transformer stacks. To put it another way, it extends our ability to compose systems using different ranges of effects.