Pre-RFC: Extending where clauses with limited formal verification

I unfortunately didn’t follow all the details about the discussion about C++20 contracts (accepted then finally rejected) [[expect]]/[[ensure]]/[[assert]]. The main issue was that different people wanted different thing from the same feature:

  • something proven at compile time (like your example) that the optimizer can rely upon
  • something asserted at run-time, that the optimizer can rely upon
  • something UB if false, that the optimizer can rely upon
  • a simple annotation for the reader, that the optimizer cannot rely upon
  • something that could be switch to compile time / runtime check / UB if false based on a compiler check.

And sometime it’s hard to tell which one is right.

For example if you have function binary_search(container, value), you expect a sorted container. In the general case, you can’t prove at compile time that the container is sorted. Checking it at runtime takes O(n) which completely remove the raison d’être of this very function. So release build should be able to turn the [[expect(self.is_sorted())]] into a no-op. Using your proposal, a static_assert() should be used (or maybe an hypothetical unchecked_assert() to be able to remove it in debug mode). Using typestates is another option (by having container.sort() returning Sorted<Self>) but with all its usual drawbacks.

At the same time, if you implement Index::index(&self, index: Idx) for your custom container, you would like to be able to add something like [[expect(self.is_valid(index))]] and it should be possible to automatically generates assert at runtime, even for release build. Having to manually write the assert at call-site totally defeat the point by requiring much more syntax compared to the current solution.


This being said, I like your proposal and I would love that someone smarter than me found a good solution that covers all use-cases.

1 Like