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