From: Ralf Jung Date: Wed, 15 Jul 2020 11:43:14 +0000 (+0200) Subject: link to 'two kinds of invariants' X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/a2ddc0ca35c1258e1a0563978a0fb1009c6ee63e?ds=sidebyside;hp=cb8b218a295d24625cdc7ecfeb9c1580cb9ff3b9 link to 'two kinds of invariants' --- diff --git a/personal/_posts/2020-07-15-unused-data.md b/personal/_posts/2020-07-15-unused-data.md index afdfff9..ccde204 100644 --- a/personal/_posts/2020-07-15-unused-data.md +++ b/personal/_posts/2020-07-15-unused-data.md @@ -30,6 +30,8 @@ fn example(b: bool) -> i32 { I hope it is not very surprising that calling `example` on, e.g., `3` transmuted to `bool` is Undefined Behavior (UB). When compiling `if`, the compiler assumes that `0` and `1` are the only possible values; there is no saying what could go wrong when that assumption is violated. +(This is a compiler-understood *validity invariant* that is fixed in the language specification, which is very different from a user-defined *safety invariant*. +See [this earlier post]({% post_url 2018-08-22-two-kinds-of-invariants.md %}) for more details on that distinction.) What is less obvious is why calling `example` on `3` is UB even when there is no such `if` being executed. To understand why that is important, let us consider the following example: