Why program this way
A subject the papers are about. The loosest grouping, and the one to reach for last.
Arguments for a way of programming rather than accounts of what a program means: Morris on designing a language so its programs can be verified, Landin on the space of languages, Dijkstra twice -- the 1968 letter on the go to statement and the 1972 notes on structured programming -- Parnas on the criteria for decomposing a system into modules, Liskov on programming with abstract data types and later, with Wing, on what subtyping has to preserve, Backus on escaping the von Neumann style, Hughes on why laziness and higher-order functions buy modularity, and Gries on deriving a program from its specification. Each is a case made to practitioners, and each is cited far more often than it is read.
Morris's *Verification Oriented Language Design* is the earliest of the arguments after Landin and the only one that argues from provability rather than from expressiveness, modularity or discipline. It is worth noticing what that implies about the others: none of them makes verifiability the reason. The set is mostly a record of the profession persuading itself on aesthetic and engineering grounds, with the formal case entered once, in 1972, in a technical report.
Gries is the partial exception and the reason he belongs here rather than only in `relatively-complete`. *The Science of Programming* teaches deriving the program from its specification, so the discipline it argues for and the calculus that justifies it are the same thing. Where Morris asks language designers to make proof possible, Gries asks programmers to work in a way that makes retrofitting unnecessary.
Parnas and Liskov are the pair to read together. Parnas gives the criterion -- decompose so that each module hides a decision likely to change -- and Liskov turns the same criterion into a language feature, then into a condition on subtyping. The argument moves from advice to mechanism across those three records, which is the clearest instance in the set of a case made to practitioners actually taking hold.
Read against `what-a-program-means`, which holds several of the same authors doing the other kind of work -- Landin, Backus and Liskov all appear in both, arguing there and explaining here.