> But that would make it fail the "eval e = eval (opt e)" rule in siraben's proof. The same for picking a different order to execute the functions in "f() + g()

> But that would make it fail the "eval e = eval (opt e)" rule in siraben's proof. The same for picking a different order to execute the functions in "f() + g()". This is really a question of how the semantics are formulated. The eval function I gave doesn't take into account an abstract machine so there is no notion of "variable allocation" or "final state" to check, the semantics doesn't account for it. To scale it to a more realistic model with nondeterminism, heaps and so on, the semantics needs to be changed to a relational one. For instance, eval would now be a relation that relates two states of the machine, and a proof of correctness would be something like[0], which takes into account all possible states of the heap. Equality would no longer used to relate two "equivalent" programs but rather some other equivalence relation with the properties one cares about, for instance two programs would be heap-equivalent if they have exactly the same effect on the heap, or UB-equivalent if they have possible UB at the "same" (again under another relation) places. [0] https://softwarefoundations.cis.upenn.edu/plf-current/Equiv.html#atrans_sound https://softwarefoundations.cis.upenn.edu/plf-current/Equiv....