We are interested mainly in rigorously specifiable properties of programs and systems; for example, in showing that a communication system can detect when all processes in a group have received a message, or showing that the processes can elect a new group coordinator when the active one fails. We might want to show that a program solves an equation or builds a new basis for a vector space.
To know that a program actually satisfies a precise property requires knowing facts in a logical theory of programs and data. Many of the key facts are mathematical theorems about abstractions - like process groups - or about data structures such as graphs - or about a class of equations. These theorems are inextricably linked to theorems about numbers, lists, trees, sets, ordered pairs, graphs and all the other basic mathematical concepts.
To know about properties of programs, we must know about a large fragment of computational mathematics. Much of this knowledge is simply taken for granted by programmers and designers, but the formal tools need access to it as well.