Formal specification of the language is definitely good to have, so lacking of it would be relatively bad, though it doesn't make the language totally unusable.
If the language has formal specification, and if we have mathematically proven compiler which guaranteed to generate code to follow that spec, we can mathematically prove our code that it doesn't violates certain rules. Some domains like airplane engine control system requires such level of safety.
The existence of a specification does not mean that the compiler is correctly implemented and free of bugs. Are mathematical proofs really possible when trading with optimization tricks and other weird compiler things? If not, the only way to know if something is ready for aviation is testing a lot.
The lack of specification is a problem if someone wants to implement a new compiler or code parser, or when the examples of the book are not sufficient to explain all the possibilities of using a given feature.
But it's extremely relevant to liability, which is a huge deal when you're dealing with (1) things that fly and (2) things that keep people alive. Formal specifications are not just technical documents; they are legal tools that limit liability. If a compiler upgrade causes a plane to crash, a formal specification (in conjunction with a contract that refers to it) can make the difference between "my fault" and "not my fault".
Of course! An optimizer is basically a huge proof engine for theorems of the form "Given the author of this code is following the rules, the observable behavior of this code is the same as that code (which has better performance)." Formalizing the spec is just about defining clearly what those rules and behavior are, so you can make statements like "this code has correct behavior when compiled with any C99 compliant compiler" instead of "eh, if it passes all the tests it'll probably be ok".