Semantics of a language describe the behaviour of a sentence in that language when executed. When you have semantics in a theorem prover you can construct equivalence proofs between programs expressed in different languages (or proofs that a compiler from one language to another is semantics preserving).

I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.