The transition from an informal problem to a formal specification is what Dijkstra in later years misgivingly called `the Pleasantness Problem' and which Naur discusses at length in Section 14 of Pluralism in Software Engineering: Turing Award Winner Peter Naur Explains. The subsequent transition, which Dijkstra took more seriously, goes from a specification to a program.
The relation between a specification and a program is similar to the relation between an abstraction and an implementation. I will now elaborate on the latter relation and I refer to Dijkstra's EWD 317: `On a methodology of design' for further details.
Consider a machine, Dijkstra says, that has a very funny adder: each integer addition takes one microsecond except when the sum formed happens to be a prime multiple of 7. In this latter case the addition takes sufficiently long that you, the programmer, cannot afford to ignore this awkward machine specific property. As a result, you try to avoid the exceptional additions as much as possible in your computations. To do so, you are forced to reason about the specific values of each integer variable in your program. This stands in sharp contrast to the ideal case where the value of an integer variable in a program need not be specified when reasoning about the program.
The fault, Dijkstra says, lies in the implementation, not in the abstraction. In his words:
[W]hen a vital abstraction is denied to a user, I call the implementation inadequate. [EWD317, p.5]
Likewise, consider a machine that does not provide dynamic stack management; that is, a machine that denies the user the vital abstraction of not having to distinguish between recursive procedures and non-recursive procedures. Then it is the machine that is inadequate and not the abstraction. In other words, keep the abstraction and wait for the better machine to be built in the near future. That's exactly how Dijkstra thought during the early 1960s, as elaborated on in my paper `Dijkstra's Rallying Cry for Generalization: the Advent of the Recursive Procedure, late 1950s -- early 1960s'.