"To some readers, these pitfalls may seem obvious, but safety holes of this sort are remarkably common in practice. ... Proper use of this technique demands caution and care:
* All invariants must be made clear to maintainers of the trusted module...
* Every change to the trusted module must be carefully audited to ensure it does not somehow weaken the desired invariants.
* Discipline is needed to resist the temptation to add unsafe trapdoors that allow compromising the invariants if used incorrectly.
* Periodic refactoring may be needed to ensure the trusted surface area remains small...
In contrast, datatypes that are correct by construction suffer none of these problems."