Didn't someone prove that the only way to prove the correctness of a program is to actually run it. Hence proving the correctness of a program is potentially a very time consuming affair.

Personally I think these kinds of languages ought to be very useful for smart contracts in the crypto currency world. When you write small chunks of code which absolutely must be correct or you will loose a ton of money then some kind of formal verification system seems attractive to me.