I agree with the overall structure of the argument but I like to think of specifications like polynomial equations defining some set of zeroes. Specifications are not really code but a good specification will cut out a definable subset of expected behaviors that can then be further refined with an executable implementation. For example, if a specification calls for a lock-free queue then there are any number of potential implementations w/ different trade-offs that I would not expect to be in the specification.

I kind of feel like the specification would call for an idealized lock free queue. Whereas the code would generate a good enough approximation of one that can be run on real hardware.

To invert your polynomial analogy, the specification might call for a sine wave, your code will generate a Taylor series approximation that is computable.