Design by Contract != Runtime Assertion

[%u]

Hello!

I just became an incredibly big fan of D; it has everything I've wanted,
except one thing:
It is said that D supports Design by Contract (DbC) programming, when in fact
what it has is runtime assertions. There is, however, a big difference. DbC
necessarily means that a compiler would have a theorem prover and would need
to prove at /Compile/-time whether or not an expression can be satisfied
(similar to what is done in the Spec# language by Microsoft Research), because
the name is /Design/ by contract. It is not the same as assertions, which
occur at run time.
I was wondering if actual design-by-contract programming (rather than mere
assertions) will be available in D at a later time?

Thank you!