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.
Algebraic types? Dependent types? You'll never see them. They're too ... research-y
Why can't those features be baked into C++ or Java?