3 ms·
No: the language defined that e.g. a NonZeroU8 can't contain 0, and the only way it could is via illegal means. You don't need a formal proof to describe that.
by dwattttt 2y ago
No: the language defined that e.g. a NonZeroU8 can't contain 0, and the only way it could is via illegal means. You don't need a formal proof to describe that.
To try to characterise what any compiler, hypothetical or not, does if you nonetheless produce one (again, via means that aren't valid) isn't meaningful.