Dependent typing can make guarantees like that if there are no loops, no parallel mutation, no I/O, no cosmic rays. For example if I made y have rand() elements

Dependent typing can make guarantees like that if there are no loops, no parallel mutation, no I/O, no cosmic rays. For example if I made y have rand() elements then there's nothing a compiler can ever do about that. In other cases the compiler can check types by executing code (not always decidable). Dependently typed languages are not Turing complete. They can help with proofs and such but it's physically impossible to use dependent types for general purpose programming (e.g. try writing Linux in Idris, you can't).