Verifiable computations (such as for cryptocurrency smart contracts) require a complete bit-precise deterministic semantic specification, which is logically isomorphic not just to computational reflection, but computational reflection with a canonical representation.
Also, Ethereum's notion of private mutable contract state seems misguided to me. A contract should have no state beyond the set of legitimate messages it received and sent as verifiable via Merkle proof on logs included (via hash) on the blockchain itself.