[Theorems about] practical programs

Any equivalence between programs in a programming language can be thought of as a theorem. Simple examples in Mathematica include:

First[Prepend[p, q]] === q

Join[Join[p, q], r] === Join[p, Join[q, r]]

Partition[Union[p], 1] === Split[Union[p]]

One can set up axiom systems say by combining definitions of programming languages with predicate logic (as done by John McCarthy for Lisp in 1963). And for programs whose structure is simple enough it has sometimes been possible to prove theorems useful for optimization or verification. But in the vast majority of cases this has been essentially impossible in practice. And I suspect that this is a reflection of widespread fundamental unprovability. In setting up programs with specific purposes there is inevitably some computational reducibility (see page 828). But I suspect that enough computational irreducibility usually remains to make unprovability common when one asks about all possible forms of behavior of the program.