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.