This seems closely related to exhaustive checking of functions. There are some functions that you can test by trying every possible input. (For example, a function that takes an int32.) But most functions can't be tested that way.

Obviously, static analysis is possible, but the type system needs to be designed with type-checking functions in mind.

Thanks, I had the same thought when I reached the word “lazy”.

The paper also describes function contracts, which I think simply ensure that the return types and argument types conform to a specification. This isn’t lazy, per se, but in a dynamic language you can’t check those things until you call the function. But isn’t that an obvious point?