[SebastianFish]

I think you are speaking to one of the core tensions in formal methods. The difference between a specification and an implementation can get blurry. Where formal methods get interesting is statically proving properties about the specification. Take a simple example of a sorting algorithm. The two most commonly proved properties of these algorithms are that they 1) return a permutation of the input list (no items removed or duplicated) and 2) that the output of the list follow some sort of ordering.

One way to look at things is to say the permutation and ordering property checkers are the specification and the actual sorting algorithm is the implementation.

To your point about the specifications being Turing complete, some tools will put restrictions on the specifications to make function termination highly likely. COQ for instance requires that recursive functions be "decreasing in their inputs" AKA that subsequent calls to the same function are passed fewer items or elements than the parent.

[NohatCoder]

Sorting is one of the more favorable tasks for being specified this way, for much code there is no simpler way to verify the output than running the same or equivalent code again.

If your specification language is not Turing complete then there is simply stuff you cannot specify. Of course, just because it isn't Turing complete doesn't mean it isn't perfectly adequate for writing bugs.