[pgcosta]

Nope. If you want to develop software for critical system(medical appliances, satellites), this should be a must. The only problem is the cost of implementation. On top of that you also have to account that there are non deterministic problems in Hoare logic, like finding the cycle invariant.