Programming languages have to be (efficiently) executable, specifications can be logical/declarative. E.g. in a specification I can state things like "forall fu

Programming languages have to be (efficiently) executable, specifications can be logical/declarative. E.g. in a specification I can state things like "forall functions, with uncomputable property foo, we have bar". Plenty of things are uncomputable (e.g. quantifiers over natural numbers), but useful in specifications. There are good and bad specifications, same as for programs. For the semantics of a programming language you could essentially transcribe an interpreter in the form of a structural operational semantics and these are relatively error prone. Instead, you could give an axiomatic semantics, which is a lot more high-level. An equivalence proof between the two gives you a high level of assurance that the operational interpretation you had in mind while writing your interpreter actually means what you think it means. A recent example, the formal specification of the weak memory model of C11 turned out to be wrong (in the sense that it forbids common compiler optimizations, because programs have access to a time machine), but this was discovered when trying to develop a program logic for C11. In practice, most broken specifications I have seen were written by people who never really worked in formal verification. I am not aware of a single instance where a piece of formally verified code was broken because of a broken specification. There are cases where the specification had to be extended. E.g. CompCert was initially developed as a whole program compiler and the spec had to be extended for separate compilation. This broke the alias analysis.