I fail to see the point of this work. When I program, what I want to see is how each statement relates a precondition to a postcondition. From this point of view, the selling point of value-oriented programming is that conditions are partially reified in the program as abstract types, rather than merely existing in the programmer's head or a separate piece of paper. Note that this does not require the complete absence of mutability: an abstract value may contain the identities of mutable objects, but the role of abstraction is to constrain the ways in which these objects can in fact mutate. Laziness is a prime example of this.