[1718627440]

I think the main point of pre- and post-conditions is, that the compiler can see them and prove that they match and will never be triggered. There probably will be a compiler flag for outputting all non-proved pre/postconditions, there is already -fanalyzer.

I think these conditions should be part of the type signature, different to what was suggested in the otherwise good talk you cited.

[AlotOfReading]

Adding conditions to the type signature would be an ABI breaking change in C++ and have nasty interactions with templates.

In general though, the compiler can't optimize across the translation unit boundary without something like LTO. The code for the callee might have already been generated by the time the caller sees that the precondition is statically satisfied.

[1718627440]

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 access through p simply becomes UB like it always was. But the contract_assume, can't be UB, since then the check and diagnostic is omitted or reordered.

[AlotOfReading]

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

whereas this would be incompatible

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

If you attach things to the prototype, then you need to sort out the compatibility rules. If contract_assume(a > 0) changes the type, the extern shouldn't be compatible. This is frequently used to allow linking against libraries compatible with older language standards while allowing newer code to benefit from newer standards like C99, C11, or C23.

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.

[1718627440]

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

However this will:

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

But this isn't a problem, since this is precisely the feature we want to introduce contracts for: catching function call mismatches that are not yet expressible in the language.

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

But I don't think anybody is arguing for that.

[zozbot234]

> the compiler can see them and prove that they match and will never be triggered

This is a huge challenge for a C-like language with pervasive global state. Might be more feasible for something like Rust, but still very difficult.

[1718627440]

You only need to check between caller and callee. If their constraints always match, it can't be triggered, if they contradict always, it will be triggered, else it can't be decided and the programmer can add annotations if he cares about, or the compiler can check what it would be like if the caller is inlined into his calling functions if that is trivial enough.