3 ms·
The UB is the result of operations which assume invariants, when they are not met. Invariants are useless if you can't assume them. Having no UB in C would requ
by eddyb 8y ago
The UB is the result of operations which assume invariants, when they are not met. Invariants are useless if you can't assume them. Having no UB in C would require having no way to break those assumptions but C is memory/type-unsafe so that's outright impossible.
Recently I've been trying to imagine what Rust's safe abstractions that use `unsafe` code internally would look like on top of some advanced mix of dependent type theory and proofs about state-manipulating imperative programs.
At that point, the optimizer would have proofs of the invariants it can rely on and it could even potentially emit proofs that every single transformation it performed preserves the (safe) semantics of the code being optimized.
But we're not there yet. Today, we need at least a small subset of the libraries of a systems language to prevent UB "by hand". And in C (or C++, although not necessarily for the same reasons), that's even harder, as there is no notion of a "safe abstraction" (one which you cannot misuse to produce UB).
- vyodaiken 8y ago>Invariants are useless if you can't assume them. I would think that what we want is invariants that have been validated, not assumed - especially not assumed incorrectly.
- eddyb 8y agoYou won't be able to entirely validate yourself most memory-related invariants in a language which can allow breaking memory safety, that's why I mentioned the hypothetical language which can encode proofs for invariants. What you want is effectively automated proof-search (a hard problem) for an entirely-safe systems language (which doesn't even exist yet, AFAIK. at least not what I described).
- vyodaiken 8y agoRight. C is not designed to be memory safe. So certain invariants are harder to prove (or just not true). One problem with UB is that it allows compilers to assume false things.