Hacker News Digest

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

Например, в случае с leftpad, многие реализации были формально верифицированы относительно свойства «длина результата равна максимуму из n и длины s», но это не гарантирует, что результат будет визуально корректным при использовании Unicode-символов.

Другая проблема — ошибки в самом инструменте верификации, хотя такие случаи редки.

Наконец, даже корректный код может вызывать ошибки, если он используется вне своих предусмотренных условий, например, при неправильной обработке исключений или при работе с системами, которые не были формально верифицированы совместно.

Таким образом, формальная верификация полезна, но требует тщательного подхода к формулировке спецификаций и понимания их ограничений.

• Обсуждение показало, что формальная верификация кода не покрывает аппаратные сбои и ограничения окружения, а также не решает проблему валидации требований пользователя.
• Участники подчеркнули, что доказательство корректности кода не защищает от ошибок в спецификации, а также не покрывает такие факторы как переполнение целочисленных типов и другие архитектурные ограничения.
• Была затронута тема различия между верификацией (verification) и валидацией (validation), где первое касается соответствия кода спецификации, а второе — решаемости реальной задачи.
• Обсуждение подняло вопрос о том, что формальные методы не покрывают такие аспекты как отказ оборудования, влияние космических лучей и другие факторы окружения, что делает их менее полезными в контексте безопасности.
• Участники также обсудили, что даже при наличии формальной верификации, остаются риски, связанные с человеческим фактором, так как спецификация может не отражать реальные требования пользователя.

• "строка" – ищет фразу целиком, без учёта регистра
• from:ник – посты конкретного автора
• lang:код – фильтр по языку (en, ru…)
• #тег – по хэштегу
• условие условие – логическое И
• условие OR условие – логическое ИЛИ
• ( ) – группировка

• Спор о «парсинге, а не валидации»: кто-то пишет собственные проверки, кто-то берёт готовые библиотеки (Zod, Clap, argparse, docopt, yargs и др.).
• Rust/PowerShell/argparse хвалят за строгие типы и понятные ошибки; JS/TS-рантайм критикуют за лишние зависимости.
• Проблема: как сообщить сразу ВСЕ ошибки, а не падать на первой; как выдавать человекочитаемые сообщения.
• «Непредставимые состояния» хороши в ядре программы, но на границе ввода нужны гибкие структуры и recovery.
• CLI ≠ API: парсим только синтаксис, доменные ограничения уносят глубже; иначе получаем перегруженный интерфейс.