Comment
Comment by jude-
Because in practice, I'm trying to reason about the consequences of submitting a given transaction. A transaction can invoke many smart contracts in addition to mine. It's not enough for my code to be correct; every piece of code the transaction causes to run has to be correct as well.