3.4 Evaluation Strategy
The confluence of our semantics enables us to soundly step statements in unusual orders. However, for an implementation, we need an actual evaluation strategy. Sequential, call-by-value evaluation would step statements in order. Lazy evaluation would work backward from the return variable, stepping statements needed to turn it into a value. By contrast, the idea of opportunistic evaluation is to step as many statements as we can, anywhere we can. Some may not be able to step yet, e.g. a function call where the function does not yet have a known definition, but we will step all the rest.
Reminds me a little of Haxl: https://engineering.fb.com/2014/06/10/web/open-sourcing-haxl...Is there a public repository with the code?