It says a sufficiently detailed spec is code. Your spec lacks details that could be added.

If you're defining "spec" that way, the word is meaningless. The point of a spec is what it doesn't say.

It's turtles all the way down. If you write your spec in C you can get pretty detailed into how sin is implemented, but not fully. The compiler is going to take your spec and still do things with it that you didn't say, like optimize it in ways you never imagined possible.

If "spec" doesn't imply that, what does it mean to you? Or maybe you are suggesting that C "code" isn't code[1] either?

[1] By the original definition of code that is actually quite true, but I think we can agree the term, as normally used, has evolved over the years?

Well, the spec can of course define constraints of how the function is implemented.