That distinction is usually captured as validation versus verification. Formal methods can verify that an implementation satisfies its specification (i.e. that we got what we asked for). To know whether the specification is reasonable/appropriate/etc. requires we validate it against our needs (i.e. that we're asking for the right thing).
Makes sense. In that context, I think that verification is nowhere near as challenging as validation when it comes to coding.
Verification is definitely a big concern for junior developers who don't know how to write good tests, however, beyond a certain level of expertise, the big challenge becomes validation.
If written properly, tests do a pretty good job at verification. Formal proofs only take care of rare edge cases (since tests can never be exhaustive), but many times, it's possible (and recommended) to write code in a way to minimize such rare edge cases anyway.
It's all about bang-for-buck: a formal proof can give me lots of confidence about some aspect of a system, but might take a long time and have a maintenance burden; if that time and maintenance could give me more confidence when used to write masses of tests instead, then it's probably better to go with the tests.
My go-to approach is property-based testing, since that can exercise edge-cases more effectively than hand-picked examples, whilst taking about the same amount of effort to write.
A couple of things in favour of "proper" formal methods (in niche circumstances):
- Sometimes the effort calculation tips in favour of a formal methods; e.g. reliably testing concurrent, distributed systems is notoriously hard, and might require even more effort than doing some proofs instead.
- Proof objects themselves, and the act of writing them, can be useful for understanding a domain or system, and why certain things are/aren't true. This doesn't apply so much for "yes/no" solvers, like SAT/SMT/resolution/etc. but is often the case for "interactive" systems like Coq/Agda.
