why do we think of the function’s code as one party, rather than the function’s invocation? checking recursive calls would still make sense to me if you think of different invocations of the same function as different parties with a contract boundary between them.

Fascinating thought. I think of contract boundaries as a lexical thing, and I was just expecting a lexical region with lexical holes in it. Contracts being run-time entities, maybe there’s some way to have them (or something like them) mediate the way a certain dynamic extent interacts with the rest of the program trace. I wonder how different that would be (if at all).

Hmm, seems like side effects are interactions between a dynamic extent (the program execution) and the rest of the program trace (the outside world), so maybe these contracts would have a relationship with effect typing.