It depends on how much logic and/or arithmetic you can get away with encoding into the type system. We abuse the heck out of it to restrict things like register & field access, state-machine transitions, and also track resource allocation/consumption. That said, it's incredibly painful to develop anything that way, and it also doesn't ultimately prevent a different problem of the "model" you've written down in the types being wrong. So, it's not a panacea, and it's incredibly difficult, but it can winnow down the surface area of potential problems and bugs... or at least move them to compile-time.