Разрыв между «доказано» и «правильно» — это спецификация

Доказательство говорит: код соответствует спецификации. Оно ничего не говорит о том, выражает ли спецификация ваше намерение.

Отсюда следуют все честные ограничения формальных методов:

• «смерть уязвимостей» — нет: неверная спецификация даёт корректный код, делающий не то;
• «QA исчезает как класс» — нет: проверять, что спецификация выражает нужное, всё равно приходится, и верифицированные проекты продолжают тестировать;
• «доказанный автопилот безопасен» — нет: автопилоты падают на восприятии (грузовик или небо), а это не логическая задача.

seL4 — верифицированное микроядро, и оно опирается на явный список допущений: железо, DMA, компилятор.

Теперь это не рассуждение, а наблюдение на своей функции. Замер 16 августа (docs/benchmark-proof-cost-2.md) поймал разрыв в дереве flang. Ведомость печатает про «Чётное» из flang/stdlib/numbers.flang:

постусловие «чётность есть делимость на два» — доказано сведением цели с телом
функции … утверждение обо ВСЕХ входах, а не о написанных

А прогон той же функции на том же дереве:

$ flang run flang/stdlib/numbers.flang --function 'Чётное' --args '{"число": -4}'
{"result":false}

Противоречия нет, и в этом вся суть: «Чётное» и «Делится на» ошибаются одинаково (обе на -0, см. minus-zero-is-a-class), и «доказано» здесь значит ровно «две ошибки согласованы обо всех входах». Спецификация была написана через вторую функцию, а не независимо, — и доказательство честно проверило именно то, что ему дали.

Почему это важно записать. Это единственная причина, по которой формальные методы за пятьдесят лет не захватили индустрию. Популярные рассказы о доказуемых языках упоминают её вскользь, а потом строят на противоположном все обещания — см. what-the-popular-stories-get-wrong.

И обратная сторона того же, найденная замером 16 августа. «Не доказано» тоже не равно «ядро слабое». Замер цены доказательства записал у функции «Противоположное»: «содержательное утверждение (результат плюс х) равен 0 ядро не взяло». Ядро право: числа flang — IEEE-754, и при х = +∞ выходит (0 − ∞) + ∞ = не число, а «не число» нулю не равно. То же на −∞ и на самом «не число». Проверено прогоном.

То есть недоказуемость была свойством УТВЕРЖДЕНИЯ, а не ядра, — и приписать её ядру значило бы завести работу, которой не нужно. Правило отсюда простое: прежде чем чинить ядро под недоказанное утверждение, прогоните утверждение на враждебной выборке (±0, ±∞, не число, пустая строка).

Связано: goal-of-the-language, condition-for-the-revolution, minus-zero-is-a-class, bottleneck-moved-to-claim-shape