TLA+ vs. Functional Languages. I once tried to understand how TLA+ could be useful if your implementation language was primarily functional (i.e., Haskell). I wrote to Leslie Lamport on his mailing list and he actually responded with what I think was a very informative dialogue: https://groups.google.com/forum/#!searchin/tlaplus/George$20...

I hope TLA+ gains more popularity. It's an interesting technology.