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

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.