Maybe I'm missing something, but how does this change anything to how it's now?

I can happily declare two completely incompatible functions with the same symbol name, as long as they are in separate TUs and I don't use -flto, neither the compiler nor the linker will complain and my program will simply be garbage. This won't change with incompatible contracts.

When I both show them to the compiler, when they contradict, the compiler will complain, that also doesn't change.

Of course this will not work:

    extern int foo(a, b);
    int foo(int a, int b) contract_assume(a > 0);

    extern int foo(a, b) contract_assume(a > 0);
    int foo(int a, int b);

> while allowing newer code to benefit from newer standards

Having no contract specified should of course result in no additional restrictions being exposed beside this already present now. This wouldn't be possible:

   foo(unsigned int a) contract_assume(possible(a < 0))