 The origin of the analysis of computation as a mathematical notion came notoriously from logic, with Hilbert's question concerning the decidability of predicate calculus, known as the Entschiedungsproblem (Hilbert and Ackermann 1950): could there be a mechanical procedure for deciding of an arbitrary sentence of logic whether it is provable? To address this question, a rigorous model of the informal concept of an effective or mechanical method in logic and mathematics was required. This is first and foremost a mathematical endeavor: one has to develop a mathematical analogue of the informal notion. Supporters of the view that computer science is mathematical in nature assume that a computer program can be seen as a physical realization of such a mathematical entity and that one can reason about programs deductively through the formal methods of theoretical computer science. Dijkstra (1974) and Hoare (1986) were very explicit in considering programs’ instructions as mathematical sentences, and considering a formal semantics for programming languages in terms of an axiomatic system (Hoare 1969). Provided that program specifications and instructions are advanced in the same formal language, formal semantics provide the means to prove correctness. Accordingly, knowledge about the behaviors of computational systems is acquired by the deductive reasoning involved in mathematical proofs of correctness. The reason at the basis of such a rationalist optimism (Eden 2007) about what can be known about computational systems is that they are artifacts, that is, human-made systems and, as such, one can predict their behaviors with certainty (Knuth 1974).