Yes! Functional or imperative programming makes no difference in his challenge problems.

Tail recursive functions and loops are the same thing. Proving a loop correct using invariants and showing (partial) correctness for a tail recursive function by (functional) induction are the same thing.