Компромисс между возможностями и гарантиями

Хиллел Уэйн формулирует это в книге Logic for Programmers: чем больше вещей способен делать язык, формат или инструмент, тем меньше он гарантирует. Он вводит эту мысль в главе о логике предикатов, кратко изложенной в predicate-logic-crash-course crash-course-predicate-logic, и отмечает, что книга возвращается к ней почти в каждой главе.

Откуда это берётся

Рассуждение начинается с кванторов. Условие some x in S: P(x) легче выполнить по мере роста S, поскольку кандидатов становится больше, а all x in S: P(x) легче выполнить по мере сжатия S. Поэтому, если S1 является подмножеством S2, логично ожидать существования предиката, который выполняется для каждого элемента S1 и нарушается для какого-то элемента S2. Этот предикат и есть то, что гарантирует S1. Если определить множество как "всё, что эта система может выразить или сделать", то ограничение множества - это способ купить гарантию.

Три примера Уэйна сопоставляют множество с его надмножеством:

• ASCII - подмножество Unicode. Каждый символ ASCII помещается в один байт, поэтому строка ABC с первого взгляда занимает три байта. В Unicode такая же на вид строка может весить шесть байт, если буквы кириллические.
• То, что программа может сделать при доступе к файлу только на чтение, - подмножество её возможностей при полном доступе. Режим только для чтения гарантирует неизменность содержимого, тогда как при полном доступе любая программа с багом может перезаписать данные.
• Формулы, построенные только из булевых значений, AND, OR и NOT, - это подмножество всех логических формул, и каждую из них можно свести к таблице истинности. Формулу some x in Nat: OddPerfectNumber(x) так выразить нельзя, и математики до сих пор не знают, истинна ли она.

Возможности с другой стороны всегда кому-то нужны. Эмодзи требуют Unicode, обновление данных требует прав на запись, а большинству интересных предикатов нужны кванторы. Компромисс - это решение о том, какая именно сторона требуется для конкретной задачи, и он вовсе не делает меньшее множество лучше в целом.

Почему бы не назвать это мощью

Уэйн отмечает, что возможности ("ability") иногда называют мощью (power), как в правиле наименьшей мощности (rule of least power - предпочитать наименее мощный язык, решающий задачу), и что слово "power" он встречал и применительно к гарантиям. Выражение "компромисс между мощью и мощью" ничего не сообщает, поэтому в книге это слово не используется вовсе.

Сама логика служит примером. Логика первого порядка запрещает помещать предикаты в множества или передавать их другим предикатам, и, по его описанию, логики высших порядков обладают большими возможностями, но меньшими гарантиями. Пропозициональная логика, где кванторов нет вовсе, находится ниже обеих - на этом уровне таблицы истинности работают всегда.

Тот же паттерн в других местах vault'а

Страницы ниже не используют термин Уэйна; взгляд на них через эту призму - оптика данной страницы.

Системные языки с безопасной работой с памятью покупают свои гарантии, уменьшая набор программ, принимаемых компилятором. memory-safety-absolutists описывает Rust как язык, отклоняющий любую программу, которая может привести к проблемам с безопасностью памяти; при этом принимается то, что компилятор иногда отвергнет совершенно корректную программу, а unsafe предлагается как способ вернуться в более широкое множество. cobaltc закрепляет эту границу в своей спецификации. Безопасный код несёт в себе перечень гарантий. Блок unsafe или вызов внешнего кода возвращает возможности, но спецификация перестаёт обещать то, что больше не может проверить, а безопасная обёртка обязана восстановить недостающие инварианты до того, как управление вернётся в безопасный код.

Базы данных идут на компромиссы по другой оси. stop-calling-databases-cp-or-ap указывает, что изоляция снимков (snapshot isolation) и MVCC намеренно нелинеаризуемы, поскольку обеспечение linearizability снизило бы уровень параллелизма, который может предложить база данных. Чтения по умолчанию в ZooKeeper опускают линеаризуемость ради скорости, а вызов sync перед операцией чтения возвращает её для этого конкретного чтения. В жертву здесь приносятся пропускная способность или задержка, а гарантией выступает степень актуальности прочитанных данных.