A formal specification for the programming language doesn't automatically verify all programs written in it; in fact it verifies none, or at most one. It serves

A formal specification for the programming language doesn't automatically verify all programs written in it; in fact it verifies none, or at most one. It serves two purposes: it defines what each language primitive does so that proofs of programs written in the lang can make use of those definitions, and sometimes it is also used to verify that a compiler indeed preserves the language's semantics, as defined in the spec, when translating it to some other language; in other words, it can be used to verify the compiler. Focusing on a formal language spec is like saying that a good way to make your software more correct is to work hard to ensure your compiler doesn't have bugs. I'm sure you'll agree there are more important things. As to use by program proofs, often an approximate ad-hoc specification is good enough. BTW, the article you linked to is about one particular formal method -- deductive proof. There are many others, with varying costs and benefits.