Formal semantics is useful primarily when you want to reason about programs.
In the past this was mainly done in programming language development (and to a lesser degree in compiler construction). Increasingly formal semantics is also used in automatic and interactive program verification, which is beginning to see industrial use. Since you are interested in compiler design, verified and certifying compilation is a hot research topic now that is based heavily on formal semantics. Check out the following systems.
X. Leroy's CompCert. This was the first verified compiler: a realistic, moderately-optimizing compiler for a large subset of the C language down to PowerPC and ARM assembly code.
The MPI's Pilsner, the first multi-pass compiler for a higher-order imperative language to be compositionally verified. Most prior work (such as CompCert) has focused on verifying whole-program compilers.
CakeML. A compiler for an ML dialect. The focus of CakeML is on minimising the trusted computing base, not on optimisation or on breadth of source language features.
- Cogent. A certified compiler from a simple functional language with linear types (useful for reasoning about memory management) to C.
Progress on such compilers has been much swifter than many (including myself) anticipated, and I expect to see more and more of this work to seep into industrial compilers.
The problem with formal semantics is rarely to write down the semantics of a language. That's usually simple. The real issue is how efficiently to prove theorems about programs in a language using the semantics.