Assertions are pessimistic, assumptions are optimistic (2014)

Rust has unreachable_unchecked and intrinsics::assume. And a clever crate that provides an assume!() macro for stating assumptions.

I toyed with them while learning some unsafe Rust by calling unsafe Windows APIs. Sometimes there were obvious relationships between function parameters and return values that my code couldn't know because the Windows API was an opaque FFI to C. Like if I ask a Windows API to fill an 8-element array, my code can assume it returns an int <= 8 instead of considering INT_MAX as a possibility.

But anything more advanced like assuming that an array's values are sorted seemed questionable. At worst, it looked like LLVM preserved expensive assumes even if they weren't useful to the optimizer.

Since it was a toy project, I didn't care. It's neat to tell my code facts about the world and imagine that a perfect code optimizer can use all those facts. Even if there's a C API in the way.

https://doc.rust-lang.org/core/hint/fn.unreachable_unchecked...

https://doc.rust-lang.org/core/intrinsics/fn.assume.html

https://crates.io/crates/assume

Discussed (a bit) at the time (sort of):

Assertions Are Pessimistic, Assumptions Are Optimistic (2014) - https://news.ycombinator.com/item?id=9828805 - July 2015 (4 comments)

I don't expect the compiler to produce "optimal" code in non-trivial cases, but being able to prove to the compiler that some high level code corresponds to some optimized assembly is high on my wishlist (obligatory list: coq, lean, framac, k-framework, f* and many others)

Brilliant. I’m actually surprised to see, nine years later, that this isn’t on track to make it into the next version of the C standard.

Is this just a different term for precondition, postcondition and invariants in "Design by Contract"?

It's not a new idea, this has been integrated into programming languages before, notably Eiffel (1985)

https://en.wikipedia.org/wiki/Design_by_contract

Assertions were a mistake. The story is always the same. Someone uses assertions to check for things that can never happen. It works as expected. Then someone else turns off assertions. Then things that cannot happen, happen, and the program thinks everything is OK.

Common Lisp type declarations work sort of like assumptions: if you DECLARE that a variable is of a specific type, the compiler is permitted to trust you on that.