Well put, thank you.

One thing I should say though is that the spec has the luxury of being free of some constraints that the implementation has. For example, the functional spec of a sorting function could describe the shape of the required output without having to say how to arrive there. Or in more complicated cases it could afford an exponential simple algorithm to say that the actual implementation must be functionally equivalent. That may make it simpler because it's free of having to run in linear or whatever time complexity.