Of course, formalisms can still be useful, but as a matter of writing style, maybe it's better to put that sort of thing in an appendix? (As sometimes done for grammars.)
With a formal spec you could also derive an implementation automatically which is a great useable reference. Look up the K framework for one possibility.
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.
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.