Personal thougth: Scala, Haskell, Coq and so little time !

There is a lot of really cool stuff going on the world in computer science and more precisely in formal proof, the last I found being: this article about "A Monadic, Functional Implementation of Real Numbers"

Haskell is continuously gaining attention, Scala and Clojure bring new dimensions to the JVM, this later (hopefully) evolving towards better support for functional paradigm and perhaps more verification support.

I'm lucky enough to have already worked in formal proof with the CompCert team when I graduated... but it was 5 years in the past.

In the meantime, I worked in the "real life business", and now I'm sure this don't feat to me. Well, at least I worked in the security domain, and discovered that their is some really hight level work done in this domain in France: two years ago, Gemalto proved a never reached level of certification for the JavaCard plateform:
http://www.gemalto.com/php/pr_view.php?id=239 . And they did it with Coq, what a coincidence :)

Well, I really want to spend a lot of more time in all these fields. So much things to do, so little time to spend in them...

EDIT: I forgot all the cool things around parallelism, Pi-Calculus, or actors (I believe there is something great that is on the way with Scala actors ;).