4 ms·

I was thinking, a function that checks for preconditions (assertions) will be necessarily slower than one that skips those checks. The code will be smaller, but

I was thinking, a function that checks for preconditions (assertions) will be necessarily slower than one that skips those checks. The code will be smaller, but not necessarily easier to read if data quality assertions are omitted. Graceful failure also can be handled on a case by case basis - something assertions don't solve. There's also a large but not unbounded search space when it comes to numerical values. Some things (like division by zero) are easy to check, but other things like valid strings or checking that a graph data structure is shaped a certain way - the search space is potentially enormous. That's why some invariants (ex: assert i <= 0) are easier to define than others (ex: i is prime) That's not to say data invariants aren't useful - our function would not work if the assumptions it depends upon aren't true. Point is, proving an invariant involves executing code, either at compile or at runtime - and there's no guaranteeing that code coming from user input or databases or remote API calls satisfy the invariant.

nerdponx 4y ago
> 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.

nerdponx 4y ago

> 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.