Steven D'Aprano writes:
(2) Self-documenting code
(3) The "Have you performed the *right* tests?" problem
Contracts are inherited, unit tests are not.
What does "inherited" mean? Just that methods that are not overridden retain their contracts?
(6) Separation of concerns: function algorithm versus error checking
Functions ought to validate their input, but doing so obfuscates the function implementation. Making that input validation a pre-condition separates the error checking and input validation from the algorithm proper, which helps make the code self-documenting.
There's nothing in the Eiffel syntax that distinguishes *which* contract(s) was (were) violated. Is there some magic? Or does the Eiffel process just die? (ISTR that is a typical error "recovery" approach in systems implemented in Eiffel, maybe from the Beautiful Code book?)
(7) You can't unit test loop invariants
I don't see how a loop invariant can be elegantly specified without mixing it in to the implementation. Can you show an example of code written in a language with support for loop invariants *not* mixed into the implementation?
(8) Executable documentation
I don't see how any of your points fail to be satisfied by use of asserts with a convention that (except for loop invariants) they're placed either at the beginning or the end of the function, depending on whether they're pre- or post-conditions. This requires a single- exit style which may sometimes be unnatural, of course.
AFAICS you can program in contract style already in Python. Contracts involving both beginning and end state would require annoying local variables, definitely. But other than that, all I see is a desire for unnecessary syntax, or stdlib, support.