this already happens, in many companies mid-level managers write the specifications (ambiguously) and other low-cost people implement them.

And when things don't work they call people like me, to try to understand the performance problems of something poorly defined and worse written.

That's exactly what we do now.

Arguably we write instructions: instead of writing out the problem and what the solution looks like, we describe a set of steps we go through—and if those steps are incorrect, there's nothing to compare against, because that was what we called the "specification".

Whether there's a difference there is in the eye of the beholder, but it does look like that specification languages such as TLA+/PlusCal/Squint or Alloy, or theorem proving languages like Coq (to be renamed Rocq) or Lean look a lot different from the likes of C, JavaScript or even Haskell.