Some of the "experimental features of static type systems" like dependent types are really powerful; you can make some strong proofs about the logic of your pro

Some of the "experimental features of static type systems" like dependent types are really powerful; you can make some strong proofs about the logic of your program. Yes, it is nice to be able to write proofs and have them checked mechanically. However, for nontrivial programs, even stating correctness (to a level of precision a proof checker can understand) is often very difficult. Once you've figured out how to do that, you still have to take the time to write the proof. There is also a cost associated with this capability even if you don't exercise it: dependent type systems (aside from things like Dependent ML, which restrict type indices to a much smaller language) tend not to play nicely with side effects like mutation, I/O, exceptions, nontermination, etc. So the proof system is not just something that's there for those times when you need it and fades away when you don't.