At least two different kinds of properties of instructions are encoded on the type level, and proven via the type checker. But are all of these properties sufficiently strict to ensure safety?