4 ms·
>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
by 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.