> The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated.

We have that for Java, too: http://www.openjml.org/

The great thing about contracts (as opposed to dependent types) is that they separate specification from verification. You could use proofs (fully- or semi-automatic), but you could also use weaker but cheaper forms of verification, such as concolic tests or randomized tests, generated from the contracts, or, weaker still, runtime assertions. Dependent types tie specification to a specific form of verification (proof).

A standardized specification language like JML can (and does) have many tools offering different forms of verification.