Well as far as I know neither language is clever enough to allow arbitrary proofs to be expressed at compile-time. (I hear that C++'s template system is Turing

Well as far as I know neither language is clever enough to allow arbitrary proofs to be expressed at compile-time. (I hear that C++'s template system is Turing-complete, which may or may not be true, but even if it is, that doesn't mean that dependent types could be expressed in a way that's easy to write/read.) So you'd have to essentially rewrite a big part of the compiler if you were to "bake dependent types" into C++ or Java, which is of course easier said than done. Not to mention that dependent types are extraordinarily complicated and have only been implemented in research systems.