Dependent types are extremely difficult to use in practice for non-experts, and more or less don't work at all on floating-point numbers. Idris and a few other

Dependent types are extremely difficult to use in practice for non-experts, and more or less don't work at all on floating-point numbers. Idris and a few other languages are working on it, but I think we are a long way off from there. Dynamic contracts solve the problem well enough for most use cases, even if they don't solve it fully.