 For Turner (2010, 2018 ch. 10), programming languages are mathematical objects defined by a formal grammar and a formal semantics. In particular, each syntactic construct, such as an assignment, a conditional or a while loop, is defined by a grammatical rule determining its syntax, and by a semantic rule associating a meaning to it. Depending on whether an operational or a denotational semantics is preferred, meaning is given in terms of respectively the operations of an abstract machine or of mathematical partial functions from set of states to set of states. For instance, the simple assignment statement \(x := E\) is associated, under an operational semantics, with the machine operation \(update(s,x,v)\) which assigns variable \(v\) interpreted as \(E\) to variable \(x\) in state \(s\). Both in the case of an operational and of a denotational semantics, programs can be understood as mathematical theories expressing the operations of an implementing machine. Consider operational semantics: a syntactic rule of the form \(\langle P,s \rangle \Downarrow s'\) states semantically that program \(P\) executed in state \(s\) results in \(s'.\) According to Turner (2010, 2018), a programming language with an operational semantics is akin to an axiomatic theory of operations in which rules provide axioms for the relation \(\Downarrow\).