I think the issue is it forces people to think about preconditions, postconditions and invariants in a very different way if they've come from imperative progra

I think the issue is it forces people to think about preconditions, postconditions and invariants in a very different way if they've come from imperative programming.