> Looking it up, I think I did that when I was 16, but I've never used it while programming.

Any reasoning about loops or recursion requires an implicit understanding of proof by induction. Making it formally explicit seems like a perfectly fine idea.