Lambda the Ultimate

Rust is systems programming languages being developed by Mozilla. It's very preliminary work, but the list of features suggests an interesting intersection of features. I'm particularly excited by the control over memory layout that Rust gives to the programmer, but it also has massive concurrency, structural typing, and the “ability to define complex invariants that hold over data structures” in its bag of tricks.

The main developer is Graydon Hoare, with contributions from heroes-to-the-Internet Dave Herman and Brendan Eich amongst others.

(seen via G. Meredith on the Scala list.)

a paper on new DbC thoughts.

Abstract. The approach known as Design by Contract (DbC) promotes reliable
software development through elaboration of type signatures for sequential programs
with logical formulae. This paper presents an assertion method which generalises the
notion of DbC to multiparty distributed interactions, enabling the specification and ver-
ification of distributed multiparty protocols, based on the π-calculus with full recursion.
Centring on the notion of global assertions and their projections onto endpoint asser-
tions, our method allows fully general specifications for typed sessions with session
channel passing, constraining the content of the exchanged messages, the choice of sub-
conversations to follow, and invariants on recursions. The paper presents key theoretical
foundations of this framework, including a validation algorithm for consistency of global
assertions and a sound and relatively complete compositional proof system for verifying
a large class of processes against assertions.

as if i'm going to grok 10% of it... but maybe it is good exercise for my grey matter.