The formal reason for separating routines into procedures and functions
is that they need different proofs of correctness. For functions, there
is no change of state and each result is a new value, so proofs are much
simpler. For procedures, there is the additional notion of old and new
values, so there is a change of state and a variable has one value at one
point in time, and a different value at a later point in time. Proof techniques
for procedures thus have to deal with time, a much more difficult problem
than functional proofs of correctness.