Sure you can! Just search exhaustively over your ultimately finite programs. There's a really simple algorithm for that, though the performance is a little wanting.

/s

(On a more serious sarcastic note, searching over your impure state space is somewhat more challenging. It's unclear how very finite it is, but I'm sure some reasonable spherical user assumptions will trim it to feasible exhaustiveness)

In Haskell, there isn't any null. The type-system ensures that a function can not receive a null value.

Functions can opt-in to the possibility of receiving 'Nothing' as a potential value. The tooling provided to Haskell can then also tell you when your function has not exhaustively handled every possible type of input (including Nothing).

In this instance, the type system provides robust automated coverage of your function's input domain w/regard to null values. Obviously type systems can't do everything, but they are the most light-weight formal methods we have.

It is true that some things you just need to test, but nullability isn't actually one of them. Many languages—including SML, Haskell, Rust, and Swift—encode nullability in the type system, so those languages can guarantee at compile-time that functions never receive null values.

You read the comment backwards. It was saying exactly that nullability of the argument is something that can be guaranteed by a type system but you can't write a test that makes sure of it.