Can one prove correctness of a function with side-effects

Question

I'm reading a lot of things about "correctness proof"* in algorithms.

Some say that proofs apply to algorithms and not implementations, but the demonstrations are done with code source most of the time, not math. And code source may have side effects. So, i would like to know if any basic principle prevent someone to prove an impure function correct.

I feel it's true, but cannot say why. If such principle exists, could you explain it ?

Thanks

* Sorry if wording is incorrect, not sure what the good one would be.

Answer 1

The answer is that, although there are no side effects in math, it is possible to mathematically model code that has side effects.

In fact, we can even pull this trick to turn impure code into pure code (without having to go to math in the first place. So, instead of the (psuedocode) function:

f(x) = {
  y := y + x
  return y
}

...we could write:

f(x, state_before) = {
  let old_y = lookup_y(state_before)
  let state_after = update_y(state_before, old_y + x)
  let new_y = lookup_y(state_after)
  return (new_y, state_after)
}

...which can accomplish the same thing with no side effects. Of course, the entire program would have to be rewritten to explicitly pass these state values around, and you'd need to write appropriate lookup_ and update_ functions for all mutable variables, but it's a theoretically straightforward process.

Of course, no one wants to program this way. (Haskell does something similar to simulate side effects without having them be part of the language, but a lot of work went into making it more ergonomic than this.) But because it can be done, we know that side-effects are a well-defined concept.

This means that we can prove things about languages with side-effects, provided that their specifications provide us with enough information to know how to rewrite programs in them into state-passing style.