> there's no guaranteeing that code coming from user input or databases or remote API calls satisfy the invariant The idea is that you should check the invaria

> there's no guaranteeing that code coming from user input or databases or remote API calls satisfy the invariant The idea is that you should check the invariant at the "boundaries" of your code. Then you can write your internal routines assuming that the invariant holds. This is a developing pattern in Idris libraries that use "proof carrying" types. You write a function that returns 'Either DataValidationError (DPair Foo fooIsValid)' and use that to construct your internal data types as well as a proof that the data satisfies whatever invariants you need. It's just an application of the "parse, don't validate" principle, extended to use dependent and proof-carrying types. The trickier scenario is when the data is already "internal" but is located outside of the application, like in a database. In that situation you either have to take the performance hit of doing internal integrity checks, or you assert that the invariant holds without checking it, and write tests accordingly + possibly out-of-band checking for data integrity. For dynamically-typed languages and/or when using runtime "contracts", I think Clojure handles this by disabling some or all precondition checks at runtime, but expects them to be turned on during testing.