Lambda the Ultimate

Just as there's been work by Connor Mcbride on Epigram, there has been work by Hongwei Xi on ATS (previously mentioned on LTU). In one of his most recent papers, to appear at ICFP 05, a type system for a language which includes proof development facilities in the type system is presented . This work has an advantage of his previous work with DML in that type system is more expressive.

Using nomads to facilitate 'destructive' updates in a functional setting feels cumbersome and hack-ish for a (semi)-functional programmer like me.
An alternative would be to use persistent data structures that exploit the non-destructive property of purely functional ones, without incurring great costs.

Chris Okasaki has been one of the few researchers that seem to have been ignoring nomads all together. Instead, he has created very interesting alternatives called 'confluently persistent data structures' for almost all the traditional ones, such as lists, arrays and maps.

Armed with these algorithms, one could build a full (relational) database engine that doesn't destroy any data, but only adds it while still being able to jump to previous versions instantly - O(1) – giving enormous scalibility, distribution and accountability advantages over traditional solutions.

I've found one implementation of such a database: Herodotus. It isn't confluently persistent however, because it only has read access to previous versions, thus making it only 'partial persistent'.
Still, I think Herodotus may be the first, but also the next step in replacing the imperative world of database technology today.