Lambda the Ultimate

A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language

I present a certified compiler from simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. I demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge automatically large parts of the proof obligations.

Software/proof source code and documentation

Slides are available from a talk I gave at the Projet Gallium seminar at INRIA Rocquencourt, in OpenOffice and PDF formats.

I found this while attempting to follow up on this post. The approach taken here—dependently-typed ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proof-carrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive big-step operational semantics, also done in Coq. Fascinating stuff.

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.