One can generate an informal spec from a formal spec.
One can NOT generate a formal spec from an informal spec (or else that “informal” spec would actually be formal, after all).
So, a formal spec is strictly better than an informal one — it enables all the benefits of an informal spec, via the ability to generate any number of informal specs from it in many human languages, cultures, levels of detail, etc., and of course enables things like compiler reproducibility (which you cannot do at all without a formal spec).
That being said, any spec is probably better than no spec.
Since many programmers are not mathematicians, a formal spec will always have a smaller audience than a well-written spec written in English. You cannot automatically derive good writing from pure mathematics.
As a result, neither is strictly better than the other. They have different audiences and serve different purposes. The audience for pure mathematics is quite small.
One can NOT generate a formal spec from an informal spec (or else that “informal” spec would actually be formal, after all).
So, a formal spec is strictly better than an informal one — it enables all the benefits of an informal spec, via the ability to generate any number of informal specs from it in many human languages, cultures, levels of detail, etc., and of course enables things like compiler reproducibility (which you cannot do at all without a formal spec).
That being said, any spec is probably better than no spec.