NaN достижим изнутри языка и делает «очевидные» правила ложными

0 делить на 0 проходит проверку типов без единой диагностики. Значит «не число» получается, ничего не нарушая, и любое правило, забывшее про него, ложно.

Как это сорвало заказ. Просили научить ядро правилу «модуль числа неотрицателен». Выглядит очевидно. Но модуль от NaN даёт NaN, а «NaN не меньше нуля» — ложь. Правило не завели.

И законная половина заказа тоже дала ноль — см. reading-if-conditions-closed-zero-goals.

Второй случай. Правило умножения нельзя было завести с посылкой «оба сомножителя ≥ 0»: +∞ не меньше 0 истинно, а 0 × ∞ даёт NaN. Завели с посылкой об обеих границах отрезка нат — тогда конечность гарантирована.

Третий случай. У остатка от деления посылок оказалось не одна, а три: знак делимого, конечность (∞ остаток от 3 — не число) и целость (2.5 остаток от 3 даёт 2.5, что больше потолка).

Правило работы. Прежде чем заказывать правило — проверить утверждение вычислением на границах: ноль, минус ноль, бесконечность, NaN, 2⁵³. Двое агентов потеряли часы на утверждениях, оказавшихся ложными.

Родственный класс — минус ноль, всплывший трижды за сутки: minus-zero-is-a-class.

Связано: double-has-no-laws, a-measured-zero-is-valuable, zero-axioms, minus-zero-is-a-class