And it is continually improving. Rust borrow checker is an example of this.
But as far as jumping into the deep end of dependent types, that's a whole other ball of wax. Like, imagine (or try!) writing leetcode solutions in Lean or Idris, with a type that proves they are correct and (bonus points) run in the specified time complexity. Even defining the hypothesis is non trivial. It's all doable, but takes orders of magnitude longer. But with dependent types you have to do it because the next function you call may require a proof that the leet function returns the thing it's supposed to.
That's just for algorithmic leet problems. Now imagine having to write proofs in a complex multithreaded system that your code is not accessing out of bounds arrays or leaking memory, and integrating libraries that each have slightly different semantics for doing the same, or they use unsigned types that make all the proofs incompatible, etc. At that point, you have to basically give up on your borrow checker and fall back to using runtime checks anyway. And even if you did get your system into a fully proved state, that only applies to that one binary; it makes no guarantees about distributed interactions, rollouts and rollbacks, or any of the other things that are the more frequent cause of bugs in production systems. In fact, it may encourage more 'distributed spaghetti" just to work around having to prove everything.
There's an analogy with how checked exceptions work in Java: cool thought, but mostly get in the way of what you're really trying to do after a while, or break things when new types of exceptions get added to the function, so everyone ends up just wrapping them with unchecked exceptions anyway. This is what would end up happening with full dependent types too, except it would pervade the entire type system and every function you write. The eventual outcome would likely be everyone just works around them (every single function, even fairly trivial ones like divide, would return an Option that the caller would have to handle or bubble up), and the actual code would be even less type safe than it would be with a simpler type system.
So, ultimately the way Rust is going, where some key things like borrow checking, are built into the language, seems to be the better approach.
But as far as jumping into the deep end of dependent types, that's a whole other ball of wax. Like, imagine (or try!) writing leetcode solutions in Lean or Idris, with a type that proves they are correct and (bonus points) run in the specified time complexity. Even defining the hypothesis is non trivial. It's all doable, but takes orders of magnitude longer. But with dependent types you have to do it because the next function you call may require a proof that the leet function returns the thing it's supposed to.
That's just for algorithmic leet problems. Now imagine having to write proofs in a complex multithreaded system that your code is not accessing out of bounds arrays or leaking memory, and integrating libraries that each have slightly different semantics for doing the same, or they use unsigned types that make all the proofs incompatible, etc. At that point, you have to basically give up on your borrow checker and fall back to using runtime checks anyway. And even if you did get your system into a fully proved state, that only applies to that one binary; it makes no guarantees about distributed interactions, rollouts and rollbacks, or any of the other things that are the more frequent cause of bugs in production systems. In fact, it may encourage more 'distributed spaghetti" just to work around having to prove everything.
There's an analogy with how checked exceptions work in Java: cool thought, but mostly get in the way of what you're really trying to do after a while, or break things when new types of exceptions get added to the function, so everyone ends up just wrapping them with unchecked exceptions anyway. This is what would end up happening with full dependent types too, except it would pervade the entire type system and every function you write. The eventual outcome would likely be everyone just works around them (every single function, even fairly trivial ones like divide, would return an Option that the caller would have to handle or bubble up), and the actual code would be even less type safe than it would be with a simpler type system.
So, ultimately the way Rust is going, where some key things like borrow checking, are built into the language, seems to be the better approach.