>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.
I would think that what we want is invariants that have been validated, not assumed - especially not assumed incorrectly.
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).