"A sample ivory program decorated with an ensures clause, checking the return value against a specification. This is a trivial case where the specification and implementation are identical."

Funny, I had a formal specification and verification course at uni, and I always felt I was writing Haskell when I was writing specifications. When you're writing Haskell to specify your Java, why not write Haskell instead and be done with it? Of course supposedly at some point it breaks down and specification won't be so trivial, but I'm not fully convinced.

The reddit thread: http://www.reddit.com/r/haskell/comments/2epdwp/ivory_langua...