No. Given a formal specification of a problem, one could use this logic to derive a correct program. In theory, that's great because it is proven error-free. In practice, of course, implementing a "correct program" can introduce bugs and running it on a non-ideal machine (i.e. any physical computer), introduces uncertainties.

Furthermore, it is expensive to do: you need people with a strong understanding of mathematics/computer science, it is time intensive, and for most applications, just writing a program is good enough. But, to be honest, that goes for most formal methods. Well, unless they're completely automated, of course.

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.

Why would it be useless?