Eiffel can promise that it will halt at runtime if a contract is violated. DT languages can promise that no contracts could ever be violated by any possible run

Eiffel can promise that it will halt at runtime if a contract is violated. DT languages can promise that no contracts could ever be violated by any possible runtime evaluation pathway. The latter is much stronger, but weird sounding. What it typically means is that you are required to not cut corners. The type system will detect your failure to handle edge cases and refuse to compile until you either handle or explicitly ignore them.