I think the key point from this is that there’s a flow:
If you have only an informal specification that’s still valuable because it lets people understand what they should expect from your code. From there, you can distil it to a formal specification. If you do that, then you have something that lets you reason about whether the design is correct, independent of the implementation. Taking a correct implementation as axiomatic, does the specification have the properties I want? If so, then the implementation may still be buggy but at least a correct implementation is possible.
The final step, actually proving that the code is a correct implementation of the specification is probably too expensive for most projects, but it’s at least possible if you have a formal specification.
Yes, I remember Plato’s Meno.