 The problem of whether computer programs are theories is tied with the relation that programs entertain with the outside world. If programs were theories, they would have to represent some empirical system, and a semantic relation would be directly established between the program and the world. By contrast, some have argued that the relation between programs and natural systems is mediated by models of the outside world (Colburn et al. 1993, Smith 1985). In particular, Smith (1985) argues that models are abstract descriptions of empirical systems, and computational systems operating in them have programs that act as models of the models, i.e., they represent abstract models of reality. Such an account of the ontology of programs comes in handy when describing the correctness problem in computer science (see  § 7):  if specifications are considered as models requiring certain behaviors from computational systems, programs can be seen as models satisfying specifications.