[o11c]

A useful way to think of this kind of thing is to hoist the assertions into the caller, where they can be optimized out.

There's a lot of poorly-explored room in compiler design to take generalized invariants/preconditions/postconditions into consideration (explicit ones are useful for opaque functions defined in a different TU), not just things considered "types" (the problem with types is that they have different lifetime/allocation concerns than assertions).

[ReleaseCandidat]

Refinement types and liquid types (which are a subclass of refinement types).

[o11c]

From what I've seen, those are poorly done in practice, usually in multiple ways.

Recently I've been writing code to deal with partial alignment. The desired invariants here typically involves at least 3 variables:

  align must be a power of 2. Since this involves only one variable, refinement types can handle this one just fine at least (expression: n && !(n & (n-1)) ).
  0 <= skew < align
    skew != 0 in some branches, additionally
  pointer_as_int(buf.start) % align == skew
    some APIs take 2 buffers that should both have the alignment
    often if the buffer points to a size-zero span at NULL, the condition does not need to hold however
  (skew + buf.len) % align == 0 (only relevant sometimes; sometimes this is a different alignment than other invariants)

Since these are, generally, separate function arguments with completely different origins, how do you apply refinement types here? Additionally, the buffer can have different kinds of external ownership; in particular, Rust's aggressive "I must move ownership without warning" makes it impossible to write a lot of good code. We must not abandon the good parts of C if you want people to actually use your stuff, even ignoring the incremental-conversion problem.

Now consider ABI compatibility, say if we had forgotten to add the skew != 0 condition somewhere. If old code calls the function, it needs to hit a thunk that verifies the condition. New code however should have done that in the caller and thus enter the code directly. Where is the compiler tooling to support this? Clearly, invariants (and pre- and post-conditions, which are just invariants for a finite time) need to be able to specify what version of your code they were first specified in. That's a lot of information to specify in a function type which often gets disregarded.