ยง Coq-club: the meaning of a specification
When I was doing my PhD, I faced questions similar to yours. It emerged from my encounter of HOL4 for completing a project after having used Coq for another. Given your question is on the meaning of a word, I would like to refer to a philosophical doctrine on how words acquire their meaning in a system of signs. Using that doctrine, I put forward how I came to an answer for myself! So turns out that a text can be perceived as a construct made around elemental "oppositions". Accordingly, textual constructs only produce meaning through their interplay of DIFFERENCES (mostly emergingin in form of binary contrasts) inside a system of distinct signs. This doctrine was first introduced by Ferdinand Saussure on which J. Derrida drew for introducing his notion of difference. Considering the above explanation, instead of hard wiring the words "specification" and "implementation" to predetermined functionality or referents, we can perceive them in a contrasting interplay whose connection is established via the proof game. The "specification" is something used by a "proof" to demonstrate "the correctness " of an "implementation ". Now going for the Saussurian doctrine, there is no problem for an expression to be specification for an implementation, but itself being an implementation for something else. Therefore, I would definitely hesitate to say it is meaningless (or even misguiding) to use the word specification in the context of formal verification. Hopefully that was useful!