... and then promptly uses pointer arithmetic to create an alias. It violated the promise.
> If you view this as 'derived from', you can never satisfy any restrict guarantee on a function whose implementation you have not carefully reviewed.
This is C, not Rust. You aren't getting proofs without careful review. You're using "restrict" in order to ask the compiler to create a faster function on the promise that it will never be used in a way that the pointers alias. It's a promise that needs to be upheld within the function and for everyone who calls the function.
Think of something like `memcpy` (overlaps not allowed) vs `memmove` (overlaps allowed). The compiler can make the first one faster, and it is your job to uphold the contract.
> As for having influence: Ralf Jung has written a PhD thesis on the correctness of Rust
Appeals to authority aren't motivating to me. I've known and worked with a whole lot of PhDs, and they aren't always right. In fact, frequently the ones I've known are overly confident when they step outside of their area of expertise.