§ 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!