> Equational reasoning is a tool for reasoning about programs, but not the only tool. Lamport uses it too, in the form of refinement
I wouldn't call refinement equational reasoning. Equational reasoning, as I understand it, is the use of value semantics for terms, within an algebra for term composition. It pretty much requires that what a computation does is encoded in the value that the term denoting it evaluates to. I'm not sure how refinement is related, as it presupposes neither value semantics nor an algebraic composition of terms. It is a relation on sequences. As in program logics like TLA all terms evaluate to TRUE or FALSE, and the algebra for combining them is boolean algebra, the argument could be made that this is a form of equational reasoning, but I don't think it is, as the boolean values that the terms evaluate to have nothing to do with values computed by the computation.
I haven't had any experience with equational reasoning, but the examples I've seen show it to be no easier than assertional reasoning, and unlike assertional reasoning it does require a particular programming style.
I wouldn't call refinement equational reasoning. Equational reasoning, as I understand it, is the use of value semantics for terms, within an algebra for term composition. It pretty much requires that what a computation does is encoded in the value that the term denoting it evaluates to. I'm not sure how refinement is related, as it presupposes neither value semantics nor an algebraic composition of terms. It is a relation on sequences. As in program logics like TLA all terms evaluate to TRUE or FALSE, and the algebra for combining them is boolean algebra, the argument could be made that this is a form of equational reasoning, but I don't think it is, as the boolean values that the terms evaluate to have nothing to do with values computed by the computation.
I haven't had any experience with equational reasoning, but the examples I've seen show it to be no easier than assertional reasoning, and unlike assertional reasoning it does require a particular programming style.