¹Since programs are referentially transparent (that is, the value of an expression depends only upon its syntactic context, not upon computation history), you can easily do equational reasoning, proof by induction, and so on.

Expressions are like theorems, definitions are like axioms, computation is like proof.