Ability-guarantee tradeoff

Hillel Wayne states it in Logic for Programmers: the more things a language, format or tool is able to do, the fewer things it guarantees. He introduces it in the chapter on predicate logic, summarized at predicate-logic-crash-course crash-course-predicate-logic, and says the book comes back to it in almost every chapter.

Where it comes from

The argument starts from quantifiers. some x in S: P(x) gets easier to satisfy as S grows, because there are more candidates, and all x in S: P(x) gets easier as S shrinks. So if S1 is a subset of S2, you should expect some predicate that holds for every element of S1 and fails for some element of S2. That predicate is what S1 guarantees. Let the set be "everything this system can express or do", and restricting it is how a guarantee gets bought.

Wayne's three examples each pair a set with a superset:

• ASCII is a subset of Unicode. Every ASCII character fits in one byte, so the string ABC is three bytes on sight. In Unicode the same-looking string can be six bytes if the letters are Cyrillic.
• What a program can do with read-only access to a file is a subset of what it can do with full access. Read-only guarantees the contents stay unchanged, while with full access any buggy program can overwrite the data.
• Formulas built only from Booleans, AND, OR and NOT are a subset of all logical formulas, and every one of them can be turned into a truth table. some x in Nat: OddPerfectNumber(x) can't, and mathematicians still don't know whether it is true.

The capability on the other side is always wanted by someone. Emoji need Unicode, updating data needs write access, and most interesting predicates need quantifiers. The tradeoff is a decision about which side a particular job needs, and it doesn't make the smaller set better in general.

Why not call it power

Wayne notes that "ability" is sometimes called power, as in the rule of least power (prefer the least powerful language that solves the task), and that he has also seen "guarantees" called power. A "power-power tradeoff" communicates nothing, so the book avoids the word altogether.

Logic itself is an instance. First-order logic forbids putting predicates in sets or passing them to other predicates, and in his description higher-order logics have more abilities and fewer guarantees. Propositional logic, with no quantifiers at all, sits below both and is the level at which truth tables always work.

The same shape elsewhere in the vault

The pages below don't use Wayne's term; reading them through it is this page's framing.

Memory-safe systems languages buy their guarantees by shrinking the set of programs a compiler accepts. memory-safety-absolutists describes Rust as refusing any program that may introduce memory-safety issues, accepting that it will sometimes reject one that was fine, and offering unsafe as the way back into the larger set. cobaltc writes that boundary into its specification. Safe code carries an enumerated list of guarantees. An unsafe block or a foreign call regains abilities, the specification stops promising what it can no longer check, and a safe wrapper must re-establish the missing invariants before control returns to safe code.

Databases trade along a different axis. stop-calling-databases-cp-or-ap points out that snapshot isolation and MVCC are non-linearizable on purpose, since enforcing linearizability would reduce the concurrency the database can offer. ZooKeeper's default reads skip linearizability for speed, and a sync call before a read buys it back for that one read. What is given up there is throughput or latency, and the guarantee is how recent a read must be.