Интересная статья про доказательство корректности программ, точнее, почему оно редко применяется на практике. TLDR:

  • Чтобы что-то доказать, нужны четкие требования и спецификация. Их получить довольно тяжело, если вообще возможно.
  • Надо понимать, что хотим получить от верификации. В бизнесе всем насрать, правильно ли у тебя сортировка работает, если клиенты не приносят бабки.
  • Надо формализовать хотелки. Человеческие понятия тяжело формализовать. Кстати, эта же проблема — причина многих проблем с безопасностью ИИ.
  • Доказывать что то формально — тяжело. Например, доказать ассоциативность сложения — либо дорого, либо опасно (например, в C++ сложение не ассоциативно в районе INT_MAX).
  • Чем язык богаче фичами, тем тяжелее в нем доказать что-то.
  • В повседневной работе хороших тестов и документации достаточно для приемлемо хорошего качества. Каждый следующий “процент качества” обычно кратно дороже предыдущего.
  • Многие проблемы лежат на уровне проектирования. Но в него почти никто не вкладывается, потому что мало кто понимает его ценность. Большой вклад вносит культурный барьер.