Sure, for somebody who is already on board with inductive reasoning and abstraction the best path in might be code. Personally I suspect "hand" has merits but I won't say there aren't other approaches.

I remain unconvinced theory-first, and "theory, the machine does it" would work out ok.

Reminded of my pascal lecturer at uni in 79 "this compiled cleanly but I haven't run it" for every coding example. He really did behave like syntactic and basic semantic checks were all you needed to prove correctness. I am sure he also knew runtime is everything.