Towards a Mathematical Science of Computation
Reference: John McCarthy (1963). “Towards a Mathematical Science of Computation.” In Information Processing 1962: Proceedings of IFIP Congress 62, North-Holland, pp. 21-28. (Version fetched is the 1996 revised reprint.) URL
Summary
McCarthy’s IFIP 1962 address sketches what a mathematical science of computation should look like, by analogy with physics: starting from basic assumptions, one should be able to deduce the important properties of the entities the science deals with. He identifies those entities as problems, procedures, data spaces, programs (which are symbolic expressions representing procedures in particular languages), and computers (viewed as finite automata, but from a stored-program-plus-unbounded-storage perspective rather than a finite-state one).
The paper enumerates the kinds of facts one would like to derive — procedure equivalence, termination, compiler correctness, program transformation preserving semantics, lower bounds — and argues that Goedel’s incompleteness precludes a complete theory but a practically adequate one is feasible. McCarthy proposes an integer-free formalism, recursive definitions via conditional expressions (the paper is a locus classicus of if p then a else b as a mathematical notation), and recursion induction as a proof method. He closes by urging that debugging be replaced by machine-checked proofs of program correctness — a foundational statement of the program-verification agenda.
Key Ideas
- Computation as a mathematical science with its own entities (problems, procedures, data spaces, programs, computers) distinct from automata theory.
- Conditional expressions
if p then a else b and recursion as the basis of a formal notation for defining functions.
- Recursion induction as a proof technique for program equivalence.
- Compiler correctness as a target theorem for the formalism.
- Debugging should be supplanted by computer-checked correctness proofs — the founding manifesto of program verification.
Connections
Conceptual Contribution
Tags