Dijkstra used the concept of program statements as "predicate transformers". The idea is that a program has a series of predicates (think "assert()" on steroid

Dijkstra used the concept of program statements as "predicate transformers". The idea is that a program has a series of predicates (think "assert()" on steroids). A predicate is a formula (usually in first order predicate logic) that characterizes the allowable states of the program at the point where the predicate appears in the program text. I.e., "N == A * k + B". Unlike assert statements, a predicate may not be executable, but rather serves as an aid to reasoning about your code. A statement (i.e., "if", "assign", "case" etc.) modifies the allowable states of the program. Hence the phrase "predicate transformer". The initial state when the program starts has a predicate that characterizes any required assumptions about the inputs. The final state has a predicate that characterizes the required output of the program upon completion. Dijkstra, Gries, Hoare, and others created formal rules of inference describing exactly how a given statement modifies the predicates. This approach worked brilliantly for the normal "structured" statements ("if", "do", etc.) (To me, the most helpful idea from their system was the idea of invariants for iterative statements.) However, their approach was impossible to do for arbitrary "goto" statements. I believe Dijkstra was of the opinion that localized, static reasoning about program correctness was (is) the best way to get code correct and error-free. The fact that arbitrary "goto" statements destroyed the ability to reason about programs in this manner was why he forcefully advocated against them. (An alternative framework, denotational semantics, includes the idea of continuations, which among other things provides a mathematically rigorous characterization of arbitrary "goto" statements.) FWIW, as a programmer I have found over the years that the predicate/"invariant" approach of Hoare-Gries-Dijkstra gives me a useful handle on reasoning through my code and getting it right.