The ABI thing is because Lisa's talk was about C++. In C, a function can have multiple declarations as long as they're compatible (as opposed to identical).

So these declarations might coexist without issue even though they have different signatures:

   extern int foo(a, b); // in include/lib.h
   int foo(int a, int b); // in src/foo.h

   const int foo(int a, int b); // "nearly" compatible

The C23 committee ran into this issue when introducing attributes. Their solution was just exclude attributes from the signature and say they're always compatible:

    Although semantically attached to a function type, the attributes described are not part of the prototype of such a function, and redeclarations and conversions that drop such an attribute are valid and constitute compatible types.

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))