There are accounts of infinitely-running programs as proofs; they have to do with the proof technique of conduction, which has to do with proving properties of

There are accounts of infinitely-running programs as proofs; they have to do with the proof technique of conduction, which has to do with proving properties of infinite data structures; a counterpart of the more familiar technique of induction, which lets you prove things about finite data structures. Side effects are a little harder to see proof-theoretically; for some effects there are reasonable stories (exceptions, for example, are a special case of continuations, which have connections to classical logic), but for many I think the story is still murky. The Curry-Howard correspondence is more of a lens through which to approach PL theory, or an evolving research agenda, than it is a settled account of all programming practice.