Right. What I'm saying is: how long do these dependently typed language features have to "incubate" before they make it into Java? Because implementations of

Right. What I'm saying is: how long do these dependently typed language features have to "incubate" before they make it into Java? Because implementations of dependently typed languages have existed for as long as Haskell has, and we've known that it's been possible to capture "proofs" in a type system for almost a century. So how much longer do you expect it will take? Or, maybe, there just isn't a real industry demand for dependent types. Hell, many engineers still have trouble convincing their employers to write robust tests, let alone full proofs of correctness.