Well, we can say "concepts" in place of "theory". And I'm comparing Eiffel with other OOP lang, not with some langs based on a solid math theory (lambda calcules for FP langs, for example). ok?
DbC is not the same as "assert macros". First, it has a lang semantic. There is an interesting graduated mechanism to turn off or turn on conditions' checking.
Dbc is not only initeresting "concept" of lang. Meyer is considering class as a type in his type system. By the way, preconditions and postconditions of class and its subclass have to be consistient. I don't remeber all details now, as I remeber preconditions of subclass are automaticly logically 'and'ed to preconditions of superclass. This supports "concept" of "class is type" and "subclass is a same type as superclass".
Other "concept" - classes are only modules.
Other "concept" - "command/query separation" = dividing functions on functions that change state of object and on functions that query some info from function (sic. pure functions!).
Other "concept" - polymorphic types (general types) - parametrisied types, including constrained parametrisied types (MAP [V, K -> HASHABLE]).
Other "concept" - solving multiple inherient problem - "name clashing"
And so on.
BTW. Why you think that Eiffel type system is unsafe? I don't what is a situation with java type now (not using java for several yeas), but I thought that java type system is more unsafe that eiffel type system. (They said that there were generic types in java).
And BTW, smalltalk is a lang with dynamic type system.
PS. In structuring programming, to prove correctness of loop construction, you have to write down precondition of loop, loop invariant, loop postcondition. You have to (mathamaticly) prove: if precondition holds than invariant holds (and in result we get solved postcondition).