> Sure, I get that, but I don't get the practical consequences for reasoning.
(0) In a language without compound values, you need to manually prove that object states faithfully represent the compound values you care about.
(1) In a dynamically typed language, you need to manually prove that computations produce the classes of values that their continuations expect.
(2) In a lazy language, you need to manually prove that variables will never be substituted with nonterminating computations.
> What's an example of something you wanted to prove in Haskell but couldn't, because it wasn't strict?
All the usual type class laws, without the pesky addendum “assuming no free variables are ever substituted with bottom, globally”. (In all fairness, strictness alone doesn't fix the problem either. At least not when laws have free variables of function type.) Redefining what variables can be substituted with is redefining the language's operational semantics, which in turn is effectively creating a new programming language. You would have to prove all the usual things from scratch: that type checking is decidable, that the type system is sound, etc.
In practice, I can still prove the things I want, but the proofs themselves are less modular in a lazy language. The problem manifests itself when you build large computations from smaller ones:
(0) In a strict language, whether any of the subcomputations terminates is a local issue, and doesn't affect the other subcomputations.
(1) In a lazy language, failure of one computation to be productive may be observed as a termination problem in a different computation.
(0) In a language without compound values, you need to manually prove that object states faithfully represent the compound values you care about.
(1) In a dynamically typed language, you need to manually prove that computations produce the classes of values that their continuations expect.
(2) In a lazy language, you need to manually prove that variables will never be substituted with nonterminating computations.
> What's an example of something you wanted to prove in Haskell but couldn't, because it wasn't strict?
All the usual type class laws, without the pesky addendum “assuming no free variables are ever substituted with bottom, globally”. (In all fairness, strictness alone doesn't fix the problem either. At least not when laws have free variables of function type.) Redefining what variables can be substituted with is redefining the language's operational semantics, which in turn is effectively creating a new programming language. You would have to prove all the usual things from scratch: that type checking is decidable, that the type system is sound, etc.
In practice, I can still prove the things I want, but the proofs themselves are less modular in a lazy language. The problem manifests itself when you build large computations from smaller ones:
(0) In a strict language, whether any of the subcomputations terminates is a local issue, and doesn't affect the other subcomputations.
(1) In a lazy language, failure of one computation to be productive may be observed as a termination problem in a different computation.