Formal Program Verification and Computabitity Theory

Whereas early researchers in computability theory described effective computability in terms of such models as Turing machines, Markov algorithms, and register machines, a recent trend has been to use simple programming languages as computability models. A parallel development to this programming approach to computability theory is the current interest in systematic and scientific development and proof of programs. This paper investigates the feasibility of using formal proofs of programs in computability theory. After describing a framework for formal verification of programs written in a simple theoretical programming language, we discuss the proofs of several typical programs used in computability theory