> I'm not sure how useful they are for reasoning about an arbitrary snippet of JS taken from the wild. Probably not much, indeed. > One problem stated in the

> I'm not sure how useful they are for reasoning about an arbitrary snippet of JS taken from the wild. Probably not much, indeed. > One problem stated in the article is we can't even rely on things like variable substitution to be effect-free I have no idea how to make sense of this. The presence or absence of effects is an object language notion. Variable substitution is an operation on the syntax of this object language, and syntax necessarily lives in a metalanguage (e.g., the language in which a compiler or interpreter is written). EDIT: Forgot about explicit substitutions, which make substitution an explicit reduction step in the object language. Even then, I don't see how substitution can be effectful by itself. > For example, in your "map" definition, the value of "f" called at the head of the list may differ from the value of "f" passed to the recursive call. At least in a call-by-value language, this is should never the case. Funny things can happen if lexical environments are first-class objects, of course.