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