Существует несколько основных моментов, почему сама постановка такого типа вопросов должна быть исключена, тем более из уст ИТ профессионалов.
Первый момент — логический
Проблема индукции, которую серьезно рассмотрел Юм, ставит под сомнение саму возможность обоснования целого ряда проблем и вопросов. Например, выведение неких общих выводов из наличия неких частных наблюдений невозможно. Неограниченное количество наблюдений чего либо, не подтверждает истинность утверждения. Карл Поппер, один из невероятнейших гениев в истории человечества, обратил внимание на проблему фальсификации, и стал автором новой парадигмы в философии науки. Какова суть проблемы фальсификации и как это касается нас? Самый известный пример, — это «Черный Лебедь». Черный Лебедь был символом невозможности чего либо в 16 веке в Лондоне. Старый Мир предполагал, что все лебеди белые, поскольку все исторические записи о лебедях описывали их белые перья. И в этом контексте черные лебеди были невозможны, или не существовали. Тем не менее, в 17 веке представитель Старого Мира встретил невозможность в Австралии.
Существует асимметрия между подтверждением и фальсификацией. Проблема индукции состоит в том, что индивидуальное утверждение, как этот лебедь белый, или делая то и то, в таком то контексте, ошибки не произошло, не может быть обобщено на универсальное утверждение. Сингулярное утверждение существования не доказывает общее.
Например, если последние 4,5 миллиарда лет Солнце регулярно (хорошо — хорошо, с неким замедлением) всходило над горизонтом, то это не говорит нам, что Солнце всегда встает над горизонтом. Или любитель парадоксов Б. Рассел приводит пример с индейкой, которую кормят, за которой ухаживают, и она думает, что так будет всегда, пока не настает тот самый день, день Благодарения.
Таким образом, чтобы доказать, что все лебеди белые, мы должны проверить всех лебедей во Вселенной, и Лейбниц мне нашептывает, что это должны быть все возможные миры, что естественно невозможно. Но для того, чтобы опровергнуть это утверждение, достаточно приехать в Австралию, и встретить одного черного лебедя. Таким образом существует фундаментальная асимметрия между подтверждением и фальсификацией.
Говорить об отсутствии багов в коде, или дыр в системе в этом контексте неверно. Нельзя даже ставить вопрос в этой плоскости, потому, что это уводит дискуссию в совершенно неверном направлении, особенно если в ней задействованы люди неиспорченные матаном.
Второй момент — вычислительный
Теорема Райса накладывает отпечаток пессимизма на нашу возможность создавать совершенные системы. Следствие теоремы Райса, которая в общем виде следует из проблемы остановки машины Тюринга и вычислимости, утверждает, что не существует универсального алгоритма для доказывания или утверждения о том, что программа, система, или алгоритм не содержит ошибок и делает то, что надо. Автоматические универсальные системы тестирования в общем невозможны. В частности да, но что бы мы ни делали, — баги будут! Статическая типизация, TDD и прочие методики могут только вселить в нас больше уверенности и избавить от некоторых страхов, не более.
Третий момент — инженерный
Существуют такие ситуации, что мы можем даже знать, что у нас существует некий специфический баг, который рушит нашу систему, потому, что мы наблюдали это в какой либо момент. Мы знаем, что баг есть. Но мы не можем его репродуцировать. Я имею в виду проблемы в мультипоточных приложениях, где правит бал недетерминизм. Нет особых проблем выловить баг, если сервер рушится каждые десять минут. Но что если нам необходимо, чтобы сервер работал несколько месяцев прежде чем проблема снова вернулась. Это в прямом смысле невозможно отладить. Хуже того, как упоминал Paul Butcher, вполне вероятно писать программы, которые содержат мультипоточные баги, которые никогда не проявятся несмотря на то, как тщательно или как долго мы бы тестировали их. Только потому, что обращения потоков к памяти могут быть переупорядочены, не означает, что так и будет сделано. И мы вполне можем быть абсолютнo в неведении о наличии проблем, пока мы не сделаем апгрейд JVM или перейдем на другое железо, где мы внезапно столкнемся с таинственными проблемами, которые никто не понимает.
Все эти три момента делают само утверждение о том, что багов нет, или о доказательстве безопасности чего либо бессмысленным. Очень большой процент ИТ профессионалов также не понимает этого. Прекрасный пример в посте Егора Бугаенко.
Если бы мне предложили на выбор две супер способности, умение делить на ноль, или находить все баги в коде, то я бы задумался, что взять, потому что это вещи одного порядка.
Комментарии (15)
HomunCulus
14.04.2017 16:39Формальная верификация это и есть вычислительный аспект. Теорема Райса применима к ней.
mrsantak
14.04.2017 16:49На самом деле есть схемы, позволяющие примерно оценивать количество не найденных ошибок в программе. Они, естественно, не способны доказать отсутствие/наличие ошибок в программе, но позволяют оценить насколько якобы безбажный/малобажный продукт в реальности неидеален.
HomunCulus
14.04.2017 16:57Да есть. Я сам когда то участвовал в разработке таких ассесмент систем для Continious Delivery pipeline.
Не помню деталей, но для проверки софта AirBus 330 (нового на тот момент) была внедрена такая система, и действительна она снизила риски и нашла много всего невкусного. Но тем не менее это были не все баги, и потом компания сталкивалась с ними в дальнейшем. Но теме не менее по результатам она себя больше чем оправдала. Извините не помню деталей в числах, поскольку давно с этой сталкивался. Вот отрывок из статьи тех времен.
https://books.google.ee/books?id=OZhCTkrCyRwC&pg=PA153&lpg=PA153&dq=AirBus+a330+software+test+history&source=bl&ots=quLKmzcdgl&sig=SosTfKgQ4GveVSjXGbxIQBIcRu8&hl=ru&sa=X&ved=0ahUKEwi-xrCtjKTTAhVEkiwKHcYqAOkQ6AEIXTAH#v=onepage&q=AirBus%20a330%20software%20test%20history&f=false
IZh
15.04.2017 01:34+2Да, проблема нерешаема в общем виде. Но всегда ли нужен общий вид?
Дано: реализовать утилиту /bin/true.
Решение:
int main(void) { return 0; }
Найдите ошибку.HomunCulus
15.04.2017 12:31Не всегда нужен общий вид. Но даже в вашем выраженном примере в действительности выполняется не этот код. Он транслируется на все более низкие уровни абстракции, где последним уровнем являются по видимому электроны, которые подчиняются законам физики и выполняют computation. Но между вашим кодом и электронами множество слоев, в том числе и операционная система, и внутреннее устройство чипа и т.д. и т.п. Это все должно приниматься во внимание.
develop7
16.04.2017 11:49Это все должно приниматься во внимание.
А оно и принимается — компиляторами, микрокодом железа, ядром ОС и библиотеками, предоставляющими интерфейс к ОС.
Balek
Формальная верификация
mrsantak
Проблема формальных доказательств в том, что нам нужно формальное описание. А еще нам нужно верифицировать формальное описание, чтобы оно соответствовало реальном миру и нашим желаниям, т.е. нам нужно формальное описание формального описания. Вытекающая из этого проблема очевидна.
В итоге формально верифицировать можно, в лучшем случае, лишь малую часть программы.
Balek
Не спорю, потому что слабо разбираюсь в теме. Но мне показалось странным, что этого нет в посте.
HomunCulus
Да это еще один импенданс между формализмом и реальным миром.
Плюс формальная верификация имеет отношение к теореме о неполноте Гёделя. Всегда будут существовать предложения которые в рамках данной формальной системы недоказуемы, или же эта система противоречива и/или неполна. По большому счету, Гёделевская неполнота, Тьюрингова остановка, оптимальность по Колмогорову это грани одной и той же проблемы. Что бы мы ни делали, решали бы проблему перебором и различными синтаксическими комбинациями формальных правил, или использовали эвристику в рамках тех же правил, нет возможности принципиально обосновать и доказать все утверждения системы.
Грубо говоря даже на арифметике мы проваливаемся в «деление на ноль»(метафора). Формальная верификация применима к очень узкому ряду проблем.
develop7
кстати, https://gist.github.com/edwinb/0047a2aff46a0f49c881 к вопросу о делении на ноль
HomunCulus
Кстати к делению на ноль.
Сложение, умножение и вычитание можно получить в арифметике Пеано с помощью примитивных рекурсивных функций. И эти операции будут всегда останавливаться. Их всего три операции. Константа(0), Функция Следования(инкремент +1) и собственно Функция Проекции (Рекурсия) которая все связывает. Три действия арифметики реализуются этими концептами. Их достаточно для реализации одного шага машины Тьюринга. Содержимое машины Тьюринга может быть представлено в виде очень большого числа и примитивные рекурсивные функции могут использоваться для чтения/записи или передвижения влево/вправо, но для полноценной работы машины Тьюринга необходимо больше. Поскольку они могут не останавливаться никогда. Также и с делением в арифметике. Когда появляется деление, то для этой операции необходима Функция Минимизации, которая уже не останавливается гарантировано. В случае же нуля, остановки не происходит, почему я и говорил, что деление на ноль и проблема остановки/тестирования это одна проблема по большому счету в Computer Science
Partial Recursive Functions
Отличная книга по этой теме.
Understanding Computation
Отрывок оттуда.