Does a Haskell program count as an inductive proof?
The statement is not true as stated. Even if we imagine a Haskell-like language where all functions terminate and values are non-bottom, only some programs would correspond to inductive proofs (as opposed to proofs not using induction), but it would be the ones that (directly or indirectly) use recursion. That said, what they are doing induction over may not at all be obvious. (For the OP: every inductive type gives rise to a notion of structural induction with "mathematical induction" just being structural induction over the naturals.) Many patterns of recursion in practical programs, e.g. quicksort, do not correspond to a direct structural induction over their inputs.

For real Haskell, for just about any program proving that it terminates for all inputs requires very strong restrictions on those inputs: all values must be fully defined and all passed in functions must terminate on at least the inputs exercised by the current program. The latter isn't checkable in general, but what we can do instead is reduce a value that stands for a putative proof to normal form, and if we succeed then we have a real proof. Unfortunately, Haskell doesn't evaluate things to normal form but only to weak head normal form. For some types we can force the weak head normal form of one expression to correspond to normal forms via rnf, but we can't do this for functions in general.

Even without restrictions, programs in Haskell correspond to proofs in some logic, albeit an inconsistent one. This leads to another aspect that they conveniently didn't elaborate on. They say that certain Haskell programs correspond to proofs of theorems, but they don't say what theorems you can state! Haskell (particularly with higher-rank polymorphism) is closely related to the polymorphic lambda calculus and that corresponds to intuitionistic, second-order propositional logic1 (SOPL) (not to be confused with second-order predicate logic which is usually what "second-order logic" refers to). While SOPL is uninteresting in the classical case, it turns out to be pretty powerful in the intuitionistic case, capable of embedding intuitionistic first-order predicate logic. The embedding is non-obvious and even with it you would not be able to prove something like the Fundamental Theorem of Arithmetic. In practice, most programs correspond to completely trivial theorems or (intutionistic) propositional tautologies.

From my (admittedly very brief) skimming of the paper, it seems that they are more interested in the Prolog-like reasoning the type class system enables than leveraging the propositions-as-types correspondence. So their comments seem to be a bit of a non sequitur anyway.

1 See Chapter 12.