4 ms·

There's a bit of an impedence mismatch with Contracts in C because C++ contracts exist partially to rectify the fact that <cassert> is broken in C++. Let's say

There's a bit of an impedence mismatch with Contracts in C because C++ contracts exist partially to rectify the fact that <cassert> is broken in C++. Let's say you have a header lib.h: inline int foo(int i) { assert(i > 0); //... } In C, this function is unspecified behavior that will probably work if the compiler is remotely sane. In C++, including this in two C++ translation units that set the NDEBUG flag differently creates an ODR violation. The C++ solution to this problem was a system where each translation unit enforces its own pre- and post- conditions (potentially 4x evaluations), and contracts act as carefully crafted exceptions to the vast number of complicated rules added on top. An example is how observable behavior is a workaround for C++ refusing to adopt C's fix for time-traveling UB. Lisa Lippincott did a great talk on this last year: https://youtu.be/yhhSW-FSWkE https://youtu.be/yhhSW-FSWkE There's not much left of Contracts once you strip away the stuff that doesn't make sense in C. I don't think you'd miss anything by simply adding hygenic macros to assert.h as the author here does, except for the 4x caller/callee verification overhead that they enforce manually. I don't think that should be enforced in the standard though. I find hidden, multiple evaluation wildly unintuitive, especially if some silly programmer accidentally writes an effectful condition.

1718627440 1y ago
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.
- zozbot234 1y ago
  > 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 1y ago
    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.
- AlotOfReading 1y ago
  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 1y ago
    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 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 1y ago
      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 1y ago

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.

zozbot234 1y ago
> 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 1y ago
  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.
AlotOfReading 1y ago
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 1y ago
  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 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 1y ago
    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.