Lambda the Ultimate

Mike Barnett, Manuel Fahndrich, K. Rustan M. Leino, Peter Muller, Wolfram Schulte, and Herman Venter, Specification and Verification: The Spec# Experience" Preprint of an article appearing in the June 2011 CACM.

CACM tagline: Can a programming language really help programmers write better programs?

Spec# is a programming system that facilitates the development of correct software. The Spec# language extends C# with contracts that allow programmers to express their design intent in the code. The Spec# tool suite consists of a compiler that emits run-time checks for contracts, a static program verifier that attempts to mathematically prove the correctness of programs, and an integration into the Visual Studio development environment. Spec# shows how contracts and verifiers can be integrated seamlessly into the software development process. This paper reflects on the six-year history of the Spec# project, scientific contributions it has made, remaining challenges for tools that seek to establish program correctness, and prospects of incorporating verification into everyday software engineering.

Spec# is, in some ways, quite similar to JML+ESC/Java2. But Spec# is a language rather than a set of annotations, which allows it to incorporate features such as a non-null type system and a very tight integration with the IDE.

Spec# was previously mentioned on LtU back in 2005.

Rob Pike's talk about the motivation for Go is rather fun, but doesn't really break new ground. Most of what he says have been said here many times, from the critic of the verbosity of C++ and Java to the skepticism about dynamic typing. Some small details are perhaps worth arguing with, but in general Pike is one of the good guys -- it's all motherhood and apple pie.

So why mention this at all (especially since it is not even breaking news)? Well, what caught my attention was the brief reconstruction of history the Pike presents. While he is perfectly honest about not being interested in history, and merely giving his personal impressions, the description is typical. What bugs me, particularly given the context of this talk, is that the history it totally sanitized. It's the "history of ideas" in the bad sense of the term -- nothing about interests (commercial and otherwise), incentives, marketing, social power, path dependence, any thing. Since we had a few discussions recently about historiography of the field, I thought I'd bring this up (the point is not to target Pike's talk in particular).

Now, when you think about Java, for example, it is very clear that the language didn't simply take over because of the reasons Pike marshals. Adoption is itself a process, and one that is worth thinking about. More to the point, I think, is that Java was (a) energetically marketed; and (b) was essentially a commercial venture, aimed at furthering the interests of a company (that is no longer with us...) Somehow I think all this is directly relevant to Go. But of course, it is hard to see Go gaining the success of Java.

All this is to say that history is not just "we had a language that did x well, but not y, so we came up with a new language, that did y but z only marginally, so now we are building Go (which compiles real fast, you know) etc. etc."

Or put differently, those who do not know history are doomed to repeat it (or some variation of this cliche that is more authentic). Or does this not hold when it comes to PLs?

Roberto Ierusalimschy, Luiz Henrique de Figueiredo, and Waldemar Celes, "Passing a Language through the Eye of a Needle: How the embeddability of Lua impacted its design", ACM Queue vol. 9, no. 5, May 2011.

A key feature of a scripting language is its ability to integrate with a system language. This integration takes two main forms: extending and embedding. In the first form, you extend the scripting language with libraries and functions written in the system language and write your main program in the scripting language. In the second form, you embed the scripting language in a host program (written in the system language) so that the host can run scripts and call functions defined in the scripts; the main program is the host program.
...
In this article we discuss how embeddability can impact the design of a language, and in particular how it impacted the design of Lua from day one. Lua is a scripting language with a particularly strong emphasis on embeddability. It has been embedded in a wide range of applications and is a leading language for scripting games.

An interesting discussion of some of the considerations that go into supporting embeddability. The design of a language clearly has an influence over the API it supports, but conversely the design of an API can have a lot of influence over the design of the language.

Kleisli Arrows of Outrageous Fortune

When we program to interact with a turbulent world, we are to some extent at its mercy. To achieve safety, we must ensure that programs act in accordance with what is known about the state of the world, as determined dynamically. Is there any hope to enforce safety policies for dynamic interaction by static typing? This paper answers with a cautious ‘yes’.

Monads provide a type discipline for effectful programming, mapping value types to computation types. If we index our types by data approximating the ‘state of the world’, we refine our values to witnesses for some condition of the world. Ordinary monads for indexed types give a discipline for effectful programming contingent on state, modelling the whims of fortune in way that Atkey’s indexed monads for ordinary types do not (Atkey, 2009). Arrows in the corresponding Kleisli category represent computations which a reach a given postcondition from a given precondition: their types are just specifications in a Hoare logic!

By way of an elementary introduction to this approach, I present the example of a monad for interacting with a file handle which is either ‘open’ or ‘closed’, constructed from a command interface specfied Hoare-style. An attempt to open a file results in a state which is statically unpredictable but dynamically detectable. Well typed programs behave accordingly in either case. Haskell’s dependent type system, as exposed by the Strathclyde Haskell Enhancement preprocessor, provides a suitable basis for this simple experiment.

I discovered this Googling around in an attempt to find some decent introductory material to Kleisli arrows. This isn't introductory, but it's a good resource. :-) The good introductory material I found was this.

In A Larger Decidable Semiunification Problem(2007), Brad Lushman and Gordon V. Cormack of University of Waterloo

[...] present a graph-theoretic framework in which to study instances of the semiunification problem (SUP), which is known to be undecidable, but has several known and important decidable subsets. One such subset, the acyclic semiunification problem (ASUP), has proved useful in the study of polymorphic type inference. We present graph-theoretic criteria in our framework that exactly characterize the ASUP acyclicity constraint. We then use our framework to find a decidable subset of SUP (which we call R-ASUP), which has a more natural description than ASUP, and strictly contains it.

Dyalog has the pleasure of announcing the start of the 2011 edition of our International APL Programming Contest. The deadline for submissions this year is August 14th, 2011. The terms and conditions, and the tasks to be solved can be found at: http://www.dyalog.com/contest_2011

The First Prize winner can look forward to US$2,500 plus a round trip travel from anywhere in the world to the Dyalog '11 Conference in Boston Massachusetts, USA, during October 2-5 2011. In addition to the grand prize, second and third prizes will be awarded with US$1,200 and US$600 respectively and a further 20 contestants will receive $100 each.

Additionally, the people or organisations that introduce the winning students to the contest will receive the same dollar prizes – and they need not be students to make the introduction. This means that you (or if you prefer, your institution) will receive an amount equal to any prizes won by students that you have referred to the competition.

The purpose of the contest is specifically to encourage students and others to investigate APL; the organisers hope that participants will find that exposure to APL broadens their horizons and adds a new tool to their toolbox. A fully featured copy of the latest release of Dyalog APL is available free of charge to students, whether or not they wish to participate in the contest.

Students of other disciplines than Computer Science are also encouraged to participate: many of the most successful APL users have backgrounds in other sciences, and have found APL to be a “Tool of Thought” for expressing solutions to problems in a wide variety of fields. Last year, the competition was won by Ryan Tarpine, a computational biologist from Brown University. We would like to thank Ryan again this year, he has been instrumental in designing the 2011 problem set, and as a result we believe that the contest this year has the most interesting (and varied) set of tasks to date.

A total of US$12,600 in prize money has been provided by several sponsors, including US-based Fiserv, Italian based APL Italiana, Danish based SimCorp and UK-based Dyalog Ltd., as well as several anonymous individuals and companies.

In One Pass Real-Time Generational Mark-Sweep Garbage Collection Joe Armstrong and Robert Virding talk about a very simple garbage collector used in Erlang*.

Traditional mark-sweep garbage collection algorithms do not allow reclamation of data until the mark phase of the algorithm has terminated. For the class of languages in which destructive operations are not allowed we can arrange that all pointers in the heap always point backwards towards "older" data. In this paper we present a simple scheme for reclaiming data for such language classes with a single pass mark-sweep collector.

We also show how the simple scheme can be modified so that the collection can be done in an incremental manner (making it suitable for real-time collection). Following this we show how the collector can be modified for generational garbage collection, and finally how the scheme can be used for a language with concurrent processes.

Unfortunately it's very restrictive. In particular even the "hidden" destructive updates used in a call-by-need language are problematic for this kind of collector.

* I'm not sure whether the described collector is still used in Erlang.

I was just lucky enough to see Peter Hawkins present a particularly compelling synthesis language: data structure synthesis:

We consider the problem of specifying combinations of data structures with complex sharing in a manner that is both declarative and results in provably correct code. In our approach, abstract data types are specified using relational algebra and functional dependencies. We describe a language of decompositions that permit the user to specify different concrete representations for relations, and show that operations on concrete representations soundly implement their relational specification. It is easy to incorporate data representations synthesized by our compiler into existing systems, leading to code that is simpler, correct by construction, and comparable in performance to the code it replaces.

As somebody experimenting with data structure representations, bringing it down to the language level is great! It'll be appearing at PLDI next month.

William Cook is documenting a new graph based "programming model" on his blog. It seems quite early in development, probably too early to offer qualified comments, but the claimed properties are interesting:

Ensō is a theoretically sound and practical reformulation of the concepts of model-driven software development. Ensō is based on first-class structural descriptions, invertable transformations, generic operations and interpretation.

Structures in Ensō are a specialized kind of graph, whose nodes are either primitive data or collections of observable properties, whose values are either nodes or collections of nodes. (snip) The key point is that structures in Ensō are viewed holistically as graphs, not as individual values or traditional sums-and-products data structures.

A structural description, or schema, specifies some of the observable properties of structures. Schemas are used to check the consistency structures. Some properties can be checked while the structure is being created, but other can only be checked once the structure is complete. Ensō allows modification of structures, which is necessary to create cyclic graphs, but also allows valid structures to be sealed to prevent further changes.

Invertible transformations are used to map one structure into another kind of structure, such that mapping can be inverted to (partially) recover the original structure from the result. One common kind of transformation is called a grammar, which is an invertible transformation between structures and text. Text grammars are invertable because they can be used for parsing and also rendering

Phil Windley whose blog posts on his startup Kynetx I sometimes mention here, since the company's product is built around a DSL, posted a nice item on reasons for designing a DSL. While partly about why people should go ahead and learn KRL, the post discusses some of the business advantages for building a product around a DSL, and some of the reasons for using and building DSLs that we here take for granted but not everyone else is cognizant of.