Formal specifications have several advantages over informal specifications.

They can be mathematically precise. They tend to be more complete than informal specifications, because the formality tends to highlight any incompleteness, which might otherwise go unnoticed.

With some kinds of formal specification, we can derive an implementation directly from the specification.

The regular expressions that describe the lexical syntax of a programming language are equivalent to a deterministic finite automaton that, when translated into executable code, provides a lexical analyzer (or scanner) for the language. Similarly, the context-free grammar of a language can be fed into a parser generator to produce a parser for the language.

The algebraic specification of an immutable abstract data type can be translated into a straightforward object-oriented implementation of the ADT. You probably did some of that translation yourself in your course on object-oriented design.

Axiomatic specifications are very generally useful, but they don’t usually give us an implementation.

The main disadvantage of formal specifications is that some programmers, users, and clients may not have the technical background needed to understand the formal specification.

Even experts who understand the formal notation will appreciate supplementary prose that gives examples and rationales.