Было много дискуссий о том, какой язык программирования лучше с точки зрения безопасности и корректности исходного кода (под «корректностью и безопасностью» мы понимаем отсутствие в программе различных ошибок, которые проявляются на этапе ее выполнения и приводят к выдаче неверного результата или неожиданному поведению). А некоторые языки программирования, такие как SPARK или OCaml, даже были специально разработаны для упрощения доказательства корректности программы.
Возможно ли вообще писать программы без ошибок?
Отсутствие ошибок ≠ корректное выполнение программы
В последнее время Rust уверенно лидирует среди безопасных языков программирования благодаря корректной работе с памятью. Существуют даже статьи на эту тему со строгими математическими доказательствами. Однако с оговоркой, что доказательство корректно, если не используются фрагменты кода, помеченные как небезопасные.
Это не критика какого-либо языка, поскольку многие забывают, что даже если предположить существование строгого математического доказательства отсутствия ошибок в программе на любом языке программирования (даже если программа самая простая, например, сложение двух чисел), программа все равно будет представлять собой некий машинный код, который должен быть выполнен на каком-либо физическом оборудовании.
Даже несколько резервных компьютеров, объединенных высоконадежным мажоритарным элементом, не обеспечивают 100% гарантии корректного выполнения экземпляра программы из-за различных внешних обстоятельств. Ведь некоторые из них не зависят от самой программы (отказ микросхемных клапанов компьютера, изменение состояния ОЗУ из-за высокоэнергетической частицы космического излучения или искра статического напряжения при уборке серверной комнаты).
В свою очередь, это означает, что даже при наличии строгого математического доказательства корректности программы после её перевода в машинный код, всё равно нет 100% гарантии выполнения конкретного экземпляра приложения без сбоев и ошибок.
Надежность выполнения приложения, а следовательно, и вероятность его сбоя из-за аппаратных проблем, может быть многократно повышена, но абсолютной она никогда не будет достигнута.
Можно считать, что написание компьютерной программы с доказанной корректностью выполнения в принципе невозможно из-за наличия различных внешних факторов, обусловленных объективными причинами нашего физического мира.
Необходима ли доказуемая программная верификация (формальная проверка кода)?
Однако это не означает, что безопасность языков программирования можно игнорировать. Просто невозможность гарантировать безошибочное выполнение экземпляра приложения ставит под сомнение необходимость предоставления доказательств математической корректности кода на любом языке программирования в ущерб всем его остальным характеристикам.
Еще одним следствием невозможности доказать корректность результата выполнения экземпляра приложения является необходимость реализации в любом языке программирования, стремящемся к корректности и безопасности разработки, средств обработки различных ситуаций возникновения ошибок в произвольные моменты времени (т. е. прерываний/исключений).
Более того, это относится даже к самым надежным и «безопасным» языкам, поскольку некорректное поведение экземпляра приложения возможно в любой части исполняемой программы, даже там, где возникновение ошибок не ожидается.
К счастью, безопасность использования конкретного языка программирования важна не только сама по себе как абсолютное значение. Она необходима как относительное значение для сравнения языков программирования друг с другом. И если невозможно достичь строго доказуемой безопасности конкретного языка программирования, то вполне возможно сравнивать их друг с другом.
Однако при их сравнении необходимо учитывать не только заявленную новым языком безопасность, но и все его остальные свойства и характеристики. Это позволит избежать ситуации, когда придётся выбросить весь старый код и переписать все программы с нуля, используя новый язык программирования.
