Lambda the Ultimate

Probably worth noting MISRA-C++. Not much to go on since you have to pay for the document that outlines the standards.

MISRA C++:2008 was finally released on June 5, 2008, following 3 years of work by a group of willing volunteers. They set out to craft a set of rules for the safe use of C++ in critical systems...

It seems not so long ago that the insurrection to fork a safer subset of C++ in Europe was suppressed. Instead of redefining the language, the efforts are now on trying to enforce coding standards and best practices. Try to solve things on the engineering side, rather than the programming language specification side.

Verifiable Functional Purity in Java. Matthew Finifter, Adrian Mettler, Naveen Sastry, and David Wagner. To appear at 15th ACM Conference on Computer and Communication Security (CCS 2008).

Proving that particular methods within a code base are functionally pure - deterministic and side-effect free - would aid verification of security properties including function invertibility, reproducibility of computation, and safety of untrusted code execution. Until now it has not been possible to automatically prove a method is functionally pure within a high-level imperative language in wide use such as Java. We discuss a technique to prove that methods are functionally pure by writing programs in a subset of Java called Joe-E; a static verifier ensures that programs fall within the subset. In Joe-E, pure methods can be trivially recognized from their method signature.

The paper includes a nice discussion of security benefits that can stem from being able to identify pure functions (of course, it is not obvious that guarantees at the programming language level are maintained at the run time level). I am sure many here have opinions about whether it makes more sense to try to graft purity on an imperative language, exposing it as an added feature, or to move programmers to functional languages..

UpgradeJ: Incremental Typechecking for Class Upgrades, Gavin Bierman, Matthew Parkinson and James Noble.

One of the problems facing developers is the constant evolution of components that are used to build applications. This evolution is typical of any multi-person or multi-site software project. How can we program in this environment? More precisely, how can language design address such evolution? In this paper we attack two significant issues that arise from constant component evolution: we propose language-level extensions that permit multiple, co-existing versions of classes and the ability to dynamically upgrade from one version of a class to another, whilst still maintaining type safety guarantees and requiring only lightweight extensions to the runtime infrastructure. We show how our extensions, whilst intuitive, provide a great deal of power by giving a number of examples. Given the subtlety of the problem, we formalize a core fragment of our language and prove a number of important safety properties.

There has been an energetic discussion of API evolution in the forum, so when I saw this paper I thought it might be of interest to LtU readers.

Ronald Loui, In Praise of Scripting: Real Programming Pragmatism, IEEE Computer, vol. 41, no. 7, July 2008. [Openly accessible draft here]

The July IEEE Computer carries an article arguing for the use of scripting languages as first programming languages, and also arguing for a greater study of what the author calls "language pragmatics" (the original article is behind the IEEE paywall, but you can find a draft that has roughly the same content here). The argument for using scripting languages as educational languages can be summed up by Loui's abstract:

The author recommends that scripting, not Java, be taught first, asserting that students should learn to love their own possibilities before they learn to loathe other people's restrictions.

The bulk of the article is devoted to exploring this basic theme in more depth, and provides an interesting contrast to the arguments in favor of moving away from Java (and scripting languages) advanced in Computer Science Education: Where Are the Software Engineers of Tomorrow? (discussed earlier on LtU here).

Loui spends the latter part of the article arguing that, in addition to syntax and semantics, research on programming language should include a formal study of language pragmatics. According to Loui, a formal study of pragmatics would address questions such as:

• What is the average lifetime of a program written in language X for programmers of type Y, for a program of type Z?
• What is the average time spent authoring versus debugging a program in language X for programmers of type Y, for a program of type Z?
• What is the consumption of short-term memory when programming in language X for programmers of type Y, for a program of type Z?

Oleg Kiselyov and Chung-chieh Shan. Lightweight Monadic Regions. Haskell'08.

We present Haskell libraries that statically ensure the safe use of resources such as file handles. We statically prevent accessing an already closed handle or forgetting to close it. The libraries can be trivially extended to other resources such as database connections and graphic contexts...

Region annotations are part of an expression's inferred type. Our new Haskell encoding of monadic regions as monad transformers needs no witness terms. It assures timely deallocation even when resources have markedly different lifetimes and the identity of the longest-living resource is determined only dynamically.

For contrast, we also implement a Haskell library for manual resource management, where deallocation is explicit and safety is assured by a form of linear types. We implement the linear typing in Haskell with the help of phantom types and a parameterized monad to statically track the type-state of resources.

I am starting to think we need a department for effect systems and related topics (though we managed without a monads department!)...

You'll probably want to read the code, so go ahead. The code makes it plain which features of the type system are needed to achieve the end result.

Catch me if you can: Towards type-safe, hierarchical, lightweight, polymorphic and efficient error management in OCaml, by David Teller, Arnaud Spiwack, Till Varoquaux:

This is the year 2008 and ML-style exceptions are everywhere. Most modern languages, whether academic or industrial, feature some variant of this mechanism. Languages such as Java even have a degree of out-of-the-box static coverage-checking for such exceptions, which is currently not available for ML languages, at least not without resorting to external tools.

In this document, we demonstrate a design principle and a tiny library for managing errors in a functional manner, with static coverage-checking, automatically-inferred, structurally typed and hierarchical exceptional cases, all of this for what we believe is a reasonable run-time cost. Our work is based on OCaml and features simple uses of higher-order programming, low-level exceptions, phantom types, polymorphic variants and compile-time code
rewriting.

Exhaustively checked, user-friendly exception handling was a bit of an open problem for awhile. As the paper details, languages supported either cumbersome, exhaustively checked polymorphic exceptions, as in Haskell, or we had unchecked easily extensible monomorphic exceptions, as in ML, or we had checked, extensible exceptions using a universal type as in Java.

Supporting exhaustively checked, easily extensible polymorphic exceptions seemed quite a challenge, which this paper solves using monadic error handling and nested polymorphic variants. The paper also gives a good overview of current techniques of exception checking in OCaml, ie. ocamlexc.

The performance of such exceptions is understandably lower than native exceptions, given all the thunking and indirection that monads entail. The authors attempt various implementations and test their performance against native exceptions. Ultimately, monadic error management seems acceptable for actual error handling, but not for control flow as native exceptions are sometimes used in OCaml.

One interesting extension is to consider how efficient the implementations would be given more sophisticated control flow operators, such as continuations, coroutines, or delimited continuations, or whether native exceptions can be salvaged using a type and effects system in place of monads.

The recent discussion around Safe and Secure Software in Ada involved some amount of discussion around what is involved in proving software secure, and what role do PLs play in this. I'd like to recommend two papers to advance this discussion:

• First, Rao & Rohatgi (2001)'s EMpowering Side-channel attacks, which discusses a fairly new technology for gathering information from running systems by monitoring their EM emissions; and
• Rae & Wildman (2003)'s A Taxonomy of Attacks on Secure Devices, which provides a synthetic classification of attacks on computer systems based on the attackers degree of access to the machinery and the attacker's objectives, and which catalogues a range of attacks into the classification.

So I hereby advance three slogans:

1. Security is physical: neither applications nor operating systems can satisfy elementary security properties, but only deployed computer systems. This is because elementary security properties are about what the attacker does, which ultimately has a physical basis;
2. Security is non-modular: Programming languages and software engineering practices can ensure that software possesses properties helpful to security, but the properties are only meaningful in the context of a strategy to ensure a computer system satisfies its security policy;
3. We should not talk of secure programming languages and secure programs, such talk does mislead; to talk instead of software being secureable might promote better understanding.

Edited following Dave Griffith's remarks.

Applied Metamodelling: A Foundation for Language Driven Development (2004)
by Tony Clark, Paul Sammut, James Willans

An excerpt:

Language-driven development is fundamentally based on the ability to rapidly design new languages and tools in a unified and interoperable manner. We argue that existing technologies do not provide this capability, but a language engineering approach based on metamodelling can. The detailed study of metamodelling and how it can realise the Language-Driven Development vision will form the focus for the remainder of this book.

In software engineering circles the term "language driven development" is synonymous with "language oriented programming", a term which LtU members are more familiar with (thanks to Martin Ward's article Language Oriented Programming which first appeared in 1994, and then Martin Fowler's essays on the topic). The book hasn't appeared on the radar here on LtU, despite 41 citations. I suspect this is due in part to only one citation at Citeseer, and the lack of cross-talk between computer scientists and software engineers.

There are a lot of similarities between the XMF language (discussion at LtU) and that of the Katahdin language (discussion at LtU). Other related discussions here at LtU, include Language Workbenches: The Killer App for DSLs - about the essay by Martin Fowler, Ralph Johnson: Language workbenches - a response to Fowler's essay, XActium - Lightweight Language Engineering? - which discusses an essay about a previous version of XMF, Generating Interpreters? , Language Oriented Programming - discusses an essay by Jetbrain's Sergey Dmitriev, "Language Oriented Programming" Meta Programming System - discussion of the Jetbrain MPS system, The DSL, MDA, UML thing again... - an older discussion on the relationship between DSLs and MDA.

(Disclaimer: Some may notice that I am mentioned on the XMF web site, but this is just because I subjected their XMF language to a number of grueling challenges which they passed with flying colors: see the language snippets in the documentation. I have no affiliation with their company.)

O'Reilly is hosting a collaborative book/wiki called Software Craftsmanship: Apprentice to Journeyman. It's structured as a series of "recipes" on how to approach different aspects of software development.

Jumbala : An Action Language for UML State Machines, Juro Dubrovin, Master's Thesis.

UML 2.0 is a language for modeling complex software systems. A UML model may describe the dynamic aspects of software as well as the static structure. We concentrate on models of reactive systems, such as embedded controllers or telecommunications switches. The behavior of such systems is modeled using UML state machines. Although UML defines the structure of state machines, it leaves open the choice of an action language,which is the language used to specify how the transitions of a state machine affect the configuration of the underlying model.

A UML action language named Jumbala is introduced. The language has been designed as part of a project where the goal is to formally analyze behavioral UML models. Jumbala is based on the Java programming language. It has nearly the same syntax and semantics for statements and expressions as Java. Some new programming constructs have been added to facilitate state machine modeling. Jumbala also supports object-oriented programming with classes and inheritance.

An interpreter that parses and executes Jumbala programs has been developed. The interpreter will be part of a prototype tool set for analyzing the behavior of reactive computer systems modeled in UML.

This is interesting because it is another example of efforts from the modeling community towards combining models and programming languages to provide a single compilable specification of software. Some of these efforts are being coordinated using the term model-driven architecture (MDA).

[edit: fixed formatting issues]