Agreed. It's more of a gradual transition towards fewer tests. The more constraints about the system you push into the type system, the less you need to test, h

Agreed. It's more of a gradual transition towards fewer tests. The more constraints about the system you push into the type system, the less you need to test, hence the dream of dependent types etc etc. You still want to have sanity checks in place in case your constraints make no sense, even if they're being correctly imposed.