"Joe-E is a subset of the Java programming language designed to support programming according to object-capability discipline." http://code.google.com/p/joe-e/

This is really interesting - it's got a lot of implications for something like doing map-reduce in Java.

When doing a Map-Reduce you can't really have any side-effects. So being able to verify this would be fairly handy.

I think another application could be software transactional memory. As far as I can tell, this more or less requires a functional implementation (since you can't roll back side-effects most of the time).

Very cool stuff.