Does your belief that "mathematics is non-strict" go as far as saying that the type of natural numbers:

    data Natural = Zero | Successor Natural

must include this member as well:

    omega :: Natural
    omega = Successor omega

    bool1 = (omega == Zero)            -- returns False
    bool2 = (omega == Successor Zero)  -- returns False
    bool3 = (omega == omega)           -- whoops, infinite loop

The moral is that some parts of mathematics may be lazy, but mathematical induction has gotta be strict. Since many functional programs rely on induction for proofs of termination, correctness and resource usage, that means they should be strict as well.

>Since many functional programs rely on induction for proofs of termination, correctness and resource usage, that means they should be strict as well.

Am I incorrect in thinking that any strict program proven to be correct and terminating is also correct as a lazy program?

Yeah, that's true for programs, i.e. things that accept no arguments. Lazy evaluation provably makes more programs terminate than any other evaluation strategy. But it's kind of misleading for functions that accept arguments, like numbers or lists. Most functions in a lazy language can fail to terminate, because the arguments could fail to terminate or could be non-standard entities like omega. So, for example, the statement "computing the length of a list always terminates" is true in a strict language but not in a lazy one.

In general, strict languages allow you to say more about termination and time/space complexity of functions than lazy languages. For example, the statement "computing the length of a list takes O(1) space" is true in a strict language, but in a lazy language it's difficult to say what the statement even means, and in most practical cases it's false. Computing length with either foldr and foldl uses at least O(n) space, and the usual advice is to use foldl', which has a strictness annotation. I think this should be alarming to anyone who recommends lazy evaluation as the right default.

In slightly more complicated cases, like sorting a list, there's no sensible way to assign a time or space complexity at all, because it depends on how the function is called and how much of the result is used by the caller. People sometimes claim that's an advantage of lazy languages, e.g. implementing quickselect in terms of quicksort and claiming that quickselect will only evaluate as much of quicksort as needed. I think that's a hack. We need to be able to reason about the time and space complexity of a program in terms of its parts, without relying on implementation details of the parts.