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
1. R. Bird (1988), "Algebraic identities for program calculation", 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.%20Intro... [PDF]
3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]