Correctness, Explanation and Intention

There appear to be two fundamentally different notions of program correctness that emanate from two different notions of program: the mathematical correctness of abstract programs and the empirical correctness of their implemented physical manifestations [2, 16, 17]. In the abstract case, a program is taken to be correct when it meets its specification. This is a mathematical affair with all the precision and clarity that follows. But physical correctness raises some concerns and puzzles that have their origins in Putnam’s notion of physical computation [15]. Moreover, these concerns would appear to effect the mathematical case. Comparing the two cases will draw out some underling philosophical issues in the traditional approaches to correctness. In particular, we examine the different concepts of explanation that accompany the different notions of correctness, and expose the underlying role of agency in both.