I'd argue that a specification must be a homomorphic version of the real code. A specification has fewer parts, but the relationships between the parts are same

I'd argue that a specification must be a homomorphic version of the real code. A specification has fewer parts, but the relationships between the parts are same as in the code. I.e. it would be interesting to write a general specification for, say, a math typesetting algorithm and then add concrete specs that describe how that algorithm materializes in, say, different instruction sets. (I wish there were such specifications, because right now when you want to understand the general principle you have to rely on texts or dig that knowledge from the idiosyncrasies of different programming languages and individual styles.) I.e. a specification that can be shared between different programming environments. Something that captures the fundamental programming principles, not the "modern" features.