I think it's more nuanced than that.

For a long-running program, like a network service or whatever, yes absolutely runtime assertions are a poor substitute.

For an impure program, where which branches of code are hit or aren't hit depends on the result of network calls, filesystem state, user input, etc, then yes, a type-system will be more powerful.

However, nix is more-or-less pure. By fully evaluating the output, you can hit all of the non-dead code, and hit every runtime assertion every time.

For a completely pure program, runtime and compiletime might as well be the same, running it and caching the output is the exact same as compiling it, and if it fails to run and outputs an error, that's the same as it failing to compile.

I know the "more-or-less pure" is doing a lot of work there, and in reality there's a lot of bits that aren't really pure, but it's close enough that a runtime type system gives you a lot more than you'd get from one in a traditional language.

This is a really good take.

I think the core caution is this is not type-level checks. Anything this validates still needs to be eval'd. It's not a guarantee of correctness for all inputs but does look to be a fairly light (and useful) tool to make unexpected states easier for you and others to identify.