> Is there some kind of reference that explains the terminology and theory you're using? On values: (0) “In call by value, the argument expression is evaluate

> Is there some kind of reference that explains the terminology and theory you're using? On values: (0) “In call by value, the argument expression is evaluated, and the resulting value is bound to the corresponding variable in the function” (https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_value https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_va...) (1) “Most languages use a call by value [evaluation] strategy, in which only outermost redexes are reduced and where a redex is reduced only when its right-hand side has already been reduced to a value - a term that has finished computing and cannot be reduced any further.” (Types and Programming Languages, p. 57) For the definition of redex, see: https://en.wikipedia.org/wiki/Reduction_strategy_(code_optimization) https://en.wikipedia.org/wiki/Reduction_strategy_(code_optim... On objects: (0) “In computer science, an object can be a variable, a data structure, or a function or a method, and as such, is a location in memory having a value and possibly referenced by an identifier.” ( https://en.wikipedia.org/wiki/Object_(computer_science) https://en.wikipedia.org/wiki/Object_(computer_science) ) In some languages, object states aren't values, though. (1) “object: a cell (unless otherwise explicitly stated)” (p. 325), “cell: a number of contiguous memory fields forming a single logical structure” (Garbage Collection: Algorithms for Automatic Dynamic Memory Management, p. 322) > It would be nice if such a reference also gave some real world examples where the terminology and theory you're using actually pays dividends, as I asked before. Compiler authors take advantage of the notion of value all the time. For example, If two expressions are guaranteed to evaluate to the same value, a compiler may emit code that evaluates the expression once, then reuses the result twice. --- Sorry, I can't reply to you directly because I'm “submitting too fast”, but: These blog posts show how to do equational reasoning on Haskell programs. (Technically, the subset of Haskell that doesn't contain nonproductive infinite loops.) http://www.haskellforall.com/2013/12/equational-reasoning.html http://www.haskellforall.com/2013/12/equational-reasoning.ht... http://www.haskellforall.com/2014/07/equational-reasoning-at-scale.html http://www.haskellforall.com/2014/07/equational-reasoning-at... http://www.haskellforall.com/2013/10/manual-proofs-for-pipes-laws.html http://www.haskellforall.com/2013/10/manual-proofs-for-pipes... Although Haskell is particularly well suited for using equational reasoning, it can also be used in other languages, provided your program primarily manipulates values, rather than objects.