A Formal Language for Analyzing Contracts

By pure serendipity I just stumbled upon this proposal, on Nick Szabo's website; it should appeal to those who found the earlier stories on Lexifi and the Composing Contracts paper interesting. It is not a fresh story (2002) but AFAIK it has not been mentioned here before; also, there is as yet no implementation.

Beyond LINQ: A Manifesto For Distributed Data-Intensive Programming

The LINQ project as embodied by C# 3.0 and Visual Basic 9 brings concepts from functional programming such as type-inference, lambda-expressions, and most importantly monad comprehensions into mainstream object-oriented programming. This is a definitively exciting for the programming language community, but realistically, it is just a tiny step towards democratizing building distributed data-intensive applications. To merely approach that goal there is still much work to do in (at least) the following areas:

Tools and IDE
It is fair to say that the the days of writing code using a text editor and batch compiler are over. Visual Studio, Eclipse, and Emacs are the norm rather than the exception. However, whenever you meet an (ex)-Smalltalk or VB6 programmer, they reminiscence the highly interactive development environment, scripters cannot live without their REPL, and tools like Ruby on Rails disrupt traditional development because of its simplicity and quick turn-around time. To simplify programming for the masses we need to shake of the yoke of the dreaded (edit, compile, run, debug)* loop and replace it with a lightweight (edit=compile=run=debug) experience.
Language and Type Systems
Writing distributed data-intensive applications naturally means dealing with many forms of data, relational, XML, objects, typed, semi-structured, or untyped. Current languages are not well equipped to deal any scrap of data, and much language and type-system innovation is required such explicit relationships, contracts,  layered type-systems, seamlessly dealing with both static and dynamic typing in the same program, extensibility, etc. The challenge is to package advanced ideas from programming language research in such a way that you do not need a PhD in type-theory to understand them.
Runtime and Libraries
Sometimes, and preferably, the compiler is able map all language and type extensions to an existing runtime such as the JVM or the CLR. However, often this is not feasible and we need to extend the runtime infrastructure to accommodate these new features. A prime example is the support for generics in the CLR versus the JVM, other examples include efficient support for first class continuations, query execution, etc. Obviously, a dynamic language is ultimately all about how dynamic the underlying runtime infrastructure is unless you emulate the dynamic features of the language, which kills interoperability. In addition to runtime support, new language and type-system features often need extensive library and infrastructure support. For example, in the context of LINQ, the language extensions are just the tip of the iceberg, and in fact the bulk of the work is in the libraries such as XLinq and in particular the OR-mapping infrastructure.
Transactions Everywhere
To make programming web services accessible to the masses, we need have to have a comprehensible way to deal with concurrency. In addition, on the desktop itself we need some way to harness the upcoming multi-core revolution. We believe that transactions are the most promising approach in this space. In fact transaction are the only way ordinary people can deal with concurrency, unless of course you are a sadomasochist who likes to wear black leather and play with locks.

As you can imagine, this is a lot of work and it will keep us language geeks off the streets for a long, long, time! And in case you are currently wandering the streets looking for a job as a compiler writer, virtual machine hacker, tool smith, etc. drop me an email. We have several job openings available.