To me there's a lot of similarities between this and type inference. "First, as we step through this program, we don’t think about specific values of x like 13

To me there's a lot of similarities between this and type inference. "First, as we step through this program, we don’t think about specific values of x like 13. Instead, we think about the set of possible values x might take on. At different points in the program, x might be an element of all integers, negative integers, or positive integers plus 0. In other words, we think of x as a symbolic value (i.e., a set of possible values) rather than a concrete value (i.e., a particular element of that set of possible values)." vs: "We expound a view of type checking as evaluation with ‘abstract values’." http://okmij.org/ftp/Computation/FLOLAC/lecture.pdf http://okmij.org/ftp/Computation/FLOLAC/lecture.pdf