Lambda the Ultimate

I am a bit reluctant to post about this, since many of the issues involved are not programming language related. I hope we can manage to avoid discussing these issues here - there are plenty of better places to discuss them.

Still, many issues that are raised in this multi-blog discussion about the performance of Rails, and Ruby in general, may be of interest from a programming language perspective. More important, in my opinion, is to put this discussion in the context of the recent revival of frameworks. We discussed many of the recent interesting libraries and frameworks. Let me point out that not only are we reaching a point where languages and frameworks are judged together (with "Ruby on Rails" a classic example), but more and more libraries make use of advanced programming techniques that were considered arcane and esoteric not long ago (e.g., jQuery use of closures, metaprogramming and code generation etc.) This is an important development, and an interesting area to keep an eye on.

The Structure and Value of Modularity in Software Design, K.J. Sullivan, W.G. Griswold, Y. Cai, B. Hallen.

The concept of information hiding modularity is a cornerstone of modern software design thought, but its formulation remains casual and its emphasis on changeability is imperfectly related to the goal of creating value in a given context. We need better models of the structure and value of information hiding, for both their explanatory power and prescriptive utility. We evaluate the potential of a new theory—developed to account for the influence of modularity on the evolution of the computer industry — to inform software design. The theory uses design structure matrices to model designs and real options techniques to value them. To test the potential utility of the theory for software we represent a model software system in its terms—Parnas’s KWIC—and evaluate the results. We contribute an extension to design structure matrices and show that the options results are consistent with Parnas’s conclusions. Our results suggest that such a theory does have potential to help inform software design.

This is really neat stuff; the authors use options theory to estimate the added value of a modular design relative to a less-modular design. It's always nice when an informal engineering intuition can be analyzed more precisely.

NixOS is a Linux distribution based on Nix, a purely functional package management system. NixOS is an experiment to see if we can build an operating system in which software packages, configuration files, boot scripts and the like are all managaed in a purely functional way, that is, they are all built by deterministic functions and they never change after they have been built. Such an operating system should have all the nice characteristics that the Nix package manager has.

Here are links to:

• the Nix package manager webpage,
• the NixOS webpage, and
• Eelco Dolstra's PhD thesis, The Purely Functional Software Deployment Model.

I found this an extremely readable thesis, light on math but high on insight. I now have an entirely new way of thinking about components and the filesystem, and that's really cool. I'd be very interested in hearing what people with serious deployment/sysadmin experience think about this approach.

(Thanks to Gavin Mendel-Gleason and Martin Bravenboer for posting the original links in the discussions page!)

After reading many posts lauding interactive tools as an integral part of the next big thing in software development, I figured I could offer this as counterpoint. The paper Magic Ink: Information Software and the Graphical Interface very eloquently argues that most software today, especially information-intensive software (think IDEs and many other GUI-based PL tools) are really badly designed. The most memorable section subtitle being interactivity considered harmlful. This is a real treasure trove of wonderful design ideas for interfaces for information-rich applications.

This paper follows in the grand tradition of Edward Tufte, whose book The Visual Display of Quantitative Information was an incredible revelation for me.

Somehow, I do think that some of the ideas behind Intentional Software fit in here -- although I make no claim as to whether the actual implementation of those ideas is an appropriate realization.

A Real-World Use of Lift

Well, lift is actually being used in production. I converted a Rails app to lift and it was a very interesting experience...

Then we did some benchmarking. For single request processing, the lift code, running inside Tomcat, ran 4 times faster than the Rails code running inside Mongrel. However, the CPU utilization was less than 5% in the lift version, where it was 100% of 1 CPU (on a dual core machine) for the Rails version. For multiple simultaneous requests being made from multiple machines, we're seeing better than 20x performance of the lift code versus the Rails code with 5 Mongrel instances. Once again, the lift code is not using very much CPU and the Rails code is pegging both CPUs.

In terms of new features, we've been able to add new features to the lift code with fewer defects than with the Rails code. Our Rails code had 70% code coverage. We discovered that anything shy of 95% code coverage with Rails means that type-os turn into runtime failures. We do not have any code coverage metrics for the lift code, but we have seen only 1 defect that's been checked in in the 2 weeks since we started using lift (vs. an average of 1 defect per checkin with the Rails code.)

So, yes, I'm pimping my own framework, and yes, I'm able to do with lift what guys like DHH are able to do with Rails, so the comparison is, in some ways, unfair.

On the other hand, Scala and lift code can be as brief and expressive as Ruby code. lift offers developers amazing productivity gains vs. traditional Java web frameworks, just as Rails does. On the other hand, lift code scales much better than Rails code. lift code is type-safe and the compiler becomes your friend (this does not mean you should not write tests, but it means that your tests can focus on the algorithm rather than making sure there are no type-os in variable and method names.)

I promise that "Dave Pollak" is not a pseudonym for "Paul Snively."

Update: I guess the self-deprecating humor hasn't worked, some 400+ reads later. Although the caveat that Dave offers about trying to objectively compare his own framework with Ruby on Rails is well-taken, I think that this nevertheless is an important marker in applying a very PLT-driven language and framework, Scala and lift, to a very realistic application, especially given that it's a rewrite from a currently-popular language and framework, Ruby and Rails. We admitted proponents of static typing and weird languages are constantly being asked for this sort of thing, and while it's doubtful that this adds anything to the PLT discussion per se—at least until we have a chance to dig into lift and see how Scala's design uniquely supports it—I thought people might find the Scala connection worth commenting on.

Scalable Statistical Bug Isolation, Ben Liblit, Mayur Naik, Alice X. Zheng, Alex Aiken, Michael I. Jordan.

We present a statistical debugging algorithm that isolates bugs in programs containing multiple undiagnosed bugs. Earlier statistical algorithms that focus solely on identifying predictors that correlate with program failure perform poorly when there are multiple bugs. Our new technique separates the effects of different bugs and identifies predictors that are associated with individual bugs. These predictors reveal both the circumstances under which bugs occur as well as the frequencies of failure modes, making it easier to prioritize debugging efforts. Our algorithm is validated using several case studies, including examples in which the algorithm identified previously unknown, significant crashing bugs in widely used systems.

This work is reminiscent of Daikon.

Expressing Heap-shape Contracts in Linear Logic, Frances Perry, Limin Jia, David Walker.

Contracts (dynamically checked programmer assertions) are a widely accepted mechanism for specifying, checking and documenting properties of software components. Most, if not all, contract systems expect programmers to use the native programming language to express their program invariants. While this is most effective for many simple invariants, expressing properties of data structures and aliasing patterns can be extremely complicated. If written in the native language in an unstructured way, such contracts are bound to be unclear and ineffective as documentation.

In this paper, we show how to use linear logic as a language of contracts for an imperative programming language. The high-level nature of our linear logical contracts makes specifying memory shape and aliasing properties of complex recursive data structures easy. Moreover, since we give our logic a clear, compositional semantics, the contracts serve as effective, executable documentation for programmer expectations. In order to evaluate the truth of our linear logical contracts at run time, we use a modifed version of LolliMon, a linear logic programming language.

This is a very elegant idea -- write assertions about heap shape using linear logic, and then check those assertions using a logic programming engine that traces the heap.

One thing this work reminds me is that I don't really understand the relationship between the way that they use the "with" connective (A & B) of linear logic and the way conjunction (A /\ B) is used in separation logic.

Increasingly, standards organizations are working on ways to improve software security. Accomplishing change through standards organizations can be harder than accomplishing change at any other organizational level, but when successful, can have a broader impact across the industry. The international standards bodies – International Organization for Standardization (ISO) and International Electro-technical Commission (IEC) – are working on a number of projects that affect software security...

This article is a useful starting point for information regarding various international standards related to the security implications of programming languages and programming practices.

Static Typing for a Faulty Lambda Calculus. David Walker. Lester Mackey. Jay Ligatti, George A. Reis, and David I. August.

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While the likelihood that such transient faults will cause any significant damage may seem remote, over the last several years transient faults have caused costly failures in high-end machines at America Online, eBay, and the Los Alamos Neutron Science Center, among others. Because susceptibility to transient faults is proportional to the size and density of transistors, the problem of transient faults will become increasingly important in the coming decades.

This paper defines the first formal, type-theoretic framework for studying reliable computation in the presence of transient faults. More specifically, it defines lambda-zap, a lambda calculus that exhibits intermittent data faults. In order to detect and recover from these faults, lambda-zap programs replicate intermediate computations and use majority voting, thereby modeling software-based fault tolerance techniques studied extensively, but informally.

To ensure that programs maintain the proper invariants and use lambda-zap primitives correctly, the paper defines a type system for the language. This type system guarantees that well-typed programs can tolerate any single data fault. To demonstrate that lambda-zap can serve as an idealized typed intermediate language, we define a type-preserving translation from a standard simply-typed lambda calculus into lambda-zap.

Lightweight static resources: Sexy types for embedded and systems programming. Oleg Kiselyov and Chung-chieh Shan.

It is an established trend to develop low-level code—embedded software, device drivers, and operating systems—using high-level languages, especially the advanced abstraction facilities in functional programming. To be reliable and secure, low-level
code must correctly manage space, time, and other resources, so special type systems and verification tools arose to regulate resource access statically. However, a general-purpose functional programming language practical today can provide the same static assurances, also with no run-time overhead. We substantiate this claim and promote the trend with two security kernels in the domain of device drivers:
1. one built around raw pointers, to track and arbitrate the size, alignment, write permission, and other properties of memory areas across indexing and casting;
2. the other built around a device register, to enforce protocol and timing requirements while reading from the register.
Our style is convenient in Haskell thanks to custom kinds and predicates (as type classes); type-level numbers, functions, and records (using functional dependencies); and mixed type- and term-level programming (enabling partial type signatures).

The related source code is also available.

Ken and Oleg's work is always worth checking out, so I urge LtU readers to go and see the solutions they propose aimed at allowing programmers of low level system software to work with raw pointers, device registers etc., while statically enforcing invariants such as pointer validity and in-bounds memory access.

The link is to a near final draft of a paper to be presented at TFP2007, and comments - I'm told - will be appreciated, especially as regards the "Related Work" section. Be quick with your comments, though, since the "camera ready" date is tomorrow...