As people keep saying, one only has to verify functions that can break invariants, e.g. if you define a type that has invariants needed by `unsafe` blocks, then

As people keep saying, one only has to verify functions that can break invariants, e.g. if you define a type that has invariants needed by `unsafe` blocks, then one has to take a close look at any functions that can modify its internals (i.e. things inside the module the type is defined). Functions that can't break these invariants because they don't have access to the internals of a type do not need to be checked: they can be assumed safe. > Well, given the most common refute of my concerns is 'you just have to make sure your unsafe blocks are verified to be correct', and the point of this article, is explicitly that this isnt the case... And, as my comment says twice, my point is just that the two cases are not very different: verifying all unsafe blocks and verifying the modules that contain `unsafe` aren't that different.