My suggestion was for C where types are for example not encoded in the name, so I thought it only matters for type checking and optimization.

> In general though, the compiler can't optimize across the translation unit boundary

Which is why I would put it in the function signature, so it is available in both translation units. Making the code match the function signature is currently generally the responsibility of the caller. For example when I declare an argument of type double and write an integer in the call, the compiler will convert it to a double on the callers side. I think the safety story will be similar to a printf-call today. A dumb compiler does nothing, the smart compiler adds a warning/error, when the precondition fails.

My understanding is, that on the callee's side this case is simply undefined behaviour. Much like it is today for example, that you can't pass a NULL everywhere, it might be declared to be UB, but currently this is only documented and internal to the callee and not documented in the function signature.

PS: This does not conflict with my other comment (https://news.ycombinator.com/user?id=1718627440), that this can't be implemented as a macro that invokes UB:

    callee (void * p, [...])
    contract_assume (nonnull (p), "p can't be NULL!")
    {
        p[0] = foo; -> UB
    }

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.