Three ways formally verified code can go wrong in practice
Несмотря на формальную верификацию, код может содержать ошибки. Одна из причин — несоответствие спецификации: доказательство может подтверждать корректность кода относительно формальной спецификации, но если сама спецификация неполна или неточно отражает реальные требования, код может работать некорректно.
Например, в случае с leftpad, многие реализации были формально верифицированы относительно свойства «длина результата равна максимуму из n и длины s», но это не гарантирует, что результат будет визуально корректным при использовании Unicode-символов.
Другая проблема — ошибки в самом инструменте верификации, хотя такие случаи редки.
Наконец, даже корректный код может вызывать ошибки, если он используется вне своих предусмотренных условий, например, при неправильной обработке исключений или при работе с системами, которые не были формально верифицированы совместно.
Таким образом, формальная верификация полезна, но требует тщательного подхода к формулировке спецификаций и понимания их ограничений.