I think of it as an alternative presentation of the same idea of induction. â€śHey 2 * 3 * 4 * 5 looks like 2 * product [3, 4, 5]â€ť is *exemplifiying* the induction proof underneath.

While we are at it, shameless plug of how I do it. To be fair, my students are 2nd/3rd year and have seen even â€śprove this inequality containing unknown constants, during the proof discover good values for the constantsâ€ť, so it is a bit more believable that you can discover code during the proof too. To be fair^2, even 50yos fear recursion as much as total newbies do.

To be sure, I got from Graham Hutton, maybe also Ralf Hinze and Richard Bird etc., the idea of starting the proof first and letting the code emerge later.

On exams, I legit give hints like â€śNotice product [2, 3, 4, 5] = 2 * 3 * 4 * 5 = 2 * product [3, 4, 5] hint hint wink winkâ€ť, albeit for tougher questions than product.