-Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers rather rely on UB to perform their optimizations.
+In the example above, what the "effective type" rule really means is that every single memory read of a `float` comes with a *proof obligation*:
+The programmer has to show that that the last write to this memory actually happened through a `float` pointer (baring some exceptions around union and character pointers).
+Similarly, the (in)famous rule that [signed integer overflow is undefined behavior](https://stackoverflow.com/questions/16188263/is-signed-integer-overflow-still-undefined-behavior-in-c) means that every single arithmetic operation on signed integers comes with the proof obligation that this operation will never, ever, overflow.
+The compiler performs its optimization under the assumption that the programmer actually went through the effort and convinced itself that this is the case.
+
+Considering that the compiler can only be so smart, this is a great way to justify optimizations that would otherwise be difficult or impossible to perform.
+Unfortunately, it is often not easy to say whether a program has undefined behavior or not -- after all, such an analysis being difficult is the entire reason compilers have to rely on UB to perform their optimizations.