3 ms·
Ah, I see what you are saying. Yes, if the optimizer is able to eliminate the postcondition check, I agree that it would constitute a proof that the code uphol
by haberman 2y ago
Ah, I see what you are saying. Yes, if the optimizer is able to eliminate the postcondition check, I agree that it would constitute a proof that the code upholds the invariant.
The big question is how much real-world code the optimizer would be capable of "solving" in this way.
I wonder if most algorithms would eventually be solvable if you keep breaking them down into smaller pieces. Or if some would have some step of irreducible complexity that the optimizer cannot figure out, now matter how much you break it down.
- saagarjha 2y agoGenerally you run into the halting problem and whatnot real quick.
- Yoric 2y agoI wonder if there is a simple way to stop compilation quickly, with a readable error message, if the optimizer isn't able to eliminate the check. edit: There is https://github.com/dtolnay/no-panic https://github.com/dtolnay/no-panic
- vlovich123 2y ago> Functions that require some amount of optimization to prove that they do not panic may no longer compile in debug mode after being marked #[no_panic]. So you’re probably going to have to protect this with a cfg_attr to only apply the no_panic in release only.
- Yoric 2y agoProbably, yes. That or forcing compilation to always target release.
- vlovich123 2y agoTo be clear, the optimizer doesn’t uphold the post condition. It just says “the post condition is usable to elide other checks”. But if the condition itself is incorrect, the compiler will STILL elide those checks. If the compiler could prove the condition on its own it would have done so. That’s why that assert is named unchecked and is itself unsafe!