> Ok, so this would mean that, according to you, it is impossible to use equational reasoning with Python programs.
You can use equational reasoning on the values that Python actually gives you: small numbers, special constants and object references.
> Whereas, according to me, it is only impossible to do this with Python programs that use mutable objects (where "mutable" here includes tuples whose slots point to mutable objects).
You can in principle use equational reasoning on programs that manipulate mutable objects. What you can't do is treat two distinct objects as equal. But, of course, in practice, you can do whatever you want. Whether your reasoning is sound is a-whole-nother matter.
> I instead have to construct a new immutable object with the same logical properties that the mutated object would have had), which makes programs harder to write, but allows me to reason rigorously about them.
No, this would be wrong. You can't use equational reasoning on objects themselves. You can only use equational reasoning on values. The value itself might be a program that manipulates objects, but you can't equate two distinct objects.
> You can't use equational reasoning on objects themselves.
I didn't say you could. I said you could use equational reasoning on programs that only manipulate immutable objects. "Immutable" means that the object's value can never change, so you can substitute the object's value for the object itself everywhere it appears in the program. Then you can apply equational reasoning to the values so obtained.
In the particular case I described, you would end up using equational reasoning on the value transformation implemented by the code that constructs the new immutable object. You would obtain that transformation, as above, by substituting object values for objects in the syntactic statement of the code.
> You can in principle use equational reasoning on programs that manipulate mutable objects.
How do you reason using an object's value if that value can change?
> "Immutable" means that the object's value can never change, so you can substitute the object's value for the object itself everywhere it appears in the program.
No, you can't. Immutable objects still have physical identities. If you want to do equational reasoning, you need to get a hold of the value itself.
> How do you reason using an object's value if that value can change?
Objects don't have “values”, they have “states”. And I said you can reason about programs that manipulate objects, not about the states of these objects. (Though maybe in a few special cases you can do the latter too.)
Is there some kind of reference that explains the terminology and theory you're using? Because it makes no sense to me as you're explaining it. 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.
(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)
(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) ) 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.)
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.
You can use equational reasoning on the values that Python actually gives you: small numbers, special constants and object references.
> Whereas, according to me, it is only impossible to do this with Python programs that use mutable objects (where "mutable" here includes tuples whose slots point to mutable objects).
You can in principle use equational reasoning on programs that manipulate mutable objects. What you can't do is treat two distinct objects as equal. But, of course, in practice, you can do whatever you want. Whether your reasoning is sound is a-whole-nother matter.
> I instead have to construct a new immutable object with the same logical properties that the mutated object would have had), which makes programs harder to write, but allows me to reason rigorously about them.
No, this would be wrong. You can't use equational reasoning on objects themselves. You can only use equational reasoning on values. The value itself might be a program that manipulates objects, but you can't equate two distinct objects.