[alibero]

In my experience, being familiar with inductive proofs is pretty useful for programming. For most non-trivial code involving recursion or loops the way I personally "know it works" usually has the flavour of an inductive proof.

For example, I might not remember how to code bisection search but I can figure out the loop invariant and from there it's easy enough to code a working binary search. And even if you have right bisection search down to muscle memory, you can modify the loop invariant to create left bisection search if you need it, while if I tried to keep two binary search algorithms in my head I feel like it would be more error-prone.