One of the characteristic features of a scientific theory is that it can explain natural phenomena and predict events. When we produce a list of numbers that indicate the direction, velocity and time for the launch of a spacecraft intended to intercept an asteroid, behind the generation of these numbers is a detailed explanation that the intercept will actually occur based on mechanics and its mathematics. But when the line of reasoning from the heavenly bodies to the decimal digits reaches the computer software and hardware used to generate these numbers, the explanation loses clarity and conviction. We come to need principles that govern the numerical approximation, the programming languages, the compilers and the hardware. These principles are not currently as well understood as those used in the physics and mathematics.
As we try to build more sophisticated software tools to solve the code creation problem and the connectivity problem, we run the risk of making the explanation of results unmanageably complex. This proposal is concerned with providing tools to manage explanations in computational science as well. The first step is to identify the new issues. We do this based on our experience and we confine the account here to matters with which we are directly familiar, but many more examples come readily to mind. After raising three kinds of problems, we focus on one kind of solution that we have explored and which we intend to pursue in more detail. We will be looking for other compatible approaches as well.
The problems we cite all have the character that they reveal a need to be more careful about the mathematical assumptions underlying the use of software. Since the computer is carrying out a wider variety of steps than just numerical evaluation, a wider variety of conditions must be generated and many more of them must be checked than is customary in derivations done by hand.
The solution we propose is the one used in mathematics when validity is an issue---be rigorous. The way to keep up with the computer's generation of conditions is to use a computer to manipulate them as well. This leads to formal methods and tools from applied logic.