> Are they talking about the same thing here? Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which

> Are they talking about the same thing here? Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which exploits the key mathematical characteristic of functional programs, that they are referentially transparent [0]. > Also, are there advantages to having such an algebra of programs outside of correctness verification? Proving correctness is a big one, but you can also use these techniques to derive more sophisticated algorithms from a naive (but correct) first implementation. For an example, see section 4 on the implementation of an efficient minimax algorithm in a short paper by Richard Bird [1]. (You will have to read some of the previous sections to understand the example.) If that piques your interest, Bird's introductory book on functional programming written with Philip Wadler [2] introduces the technique, which is usually called "program calculation". (Though published in 1988, their book remains a great introduction to functional programming.) If you really want to go off the deep end, Jeremy Gibbons's extensive lectures notes, published as a book chapter [3], are the best source I know. (Beware: here be category theory.) 0. https://en.m.wikipedia.org/wiki/Referential_transparency https://en.m.wikipedia.org/wiki/Referential_transparency 1. R. Bird (1988), "Algebraic identities for program calculation", http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf [PDF] 2. R. Bird and P. Wadler (1988), Introduction to Functional Programming. It's out of print and hard copies are scarce, but a scan is available at https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Introduction%20to%20Functional%20Programming.1ed.pdf https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro... [PDF] 3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]