Сегодня просматривая публикацию Егора Бугаенко When Do You Stop Testing!, с удивлением обнаружил, что немногие понимают и задумываются о том, что проблема тестирования и утверждения того, что система не имеет недостатков принципиально не решаема. Это кстати еще актуально и в связи с внедрением электронных выборов, и требованиями со стороны официальных лиц и журналистов доказательств отсутствия дыр в системе безопасности. Например у нас (Эстония) эта дискуссия идет полным ходом, и политики хотят получить стопроцентные доказательства надежности системы электронных выборов. Публичные политики, как правило незнакомы с логикой в её формальном виде. А Юм и Поппер, в лучшем случае, напоминают о каких то скучных философских семинарах, о которых лучше забыть. Но когда я слышу о том, что тестер или сеньор начинает вполне серьезно доказывать, что код протестирован и ошибок нет совсем, мое лицо приобретает это выражение:
Существует несколько основных моментов, почему сама постановка такого типа вопросов должна быть исключена, тем более из уст ИТ профессионалов.
Проблема индукции, которую серьезно рассмотрел Юм, ставит под сомнение саму возможность обоснования целого ряда проблем и вопросов. Например, выведение неких общих выводов из наличия неких частных наблюдений невозможно. Неограниченное количество наблюдений чего либо, не подтверждает истинность утверждения. Карл Поппер, один из невероятнейших гениев в истории человечества, обратил внимание на проблему фальсификации, и стал автором новой парадигмы в философии науки. Какова суть проблемы фальсификации и как это касается нас? Самый известный пример, — это «Черный Лебедь». Черный Лебедь был символом невозможности чего либо в 16 веке в Лондоне. Старый Мир предполагал, что все лебеди белые, поскольку все исторические записи о лебедях описывали их белые перья. И в этом контексте черные лебеди были невозможны, или не существовали. Тем не менее, в 17 веке представитель Старого Мира встретил невозможность в Австралии.
Существует асимметрия между подтверждением и фальсификацией. Проблема индукции состоит в том, что индивидуальное утверждение, как этот лебедь белый, или делая то и то, в таком то контексте, ошибки не произошло, не может быть обобщено на универсальное утверждение. Сингулярное утверждение существования не доказывает общее.
Например, если последние 4,5 миллиарда лет Солнце регулярно (хорошо — хорошо, с неким замедлением) всходило над горизонтом, то это не говорит нам, что Солнце всегда встает над горизонтом. Или любитель парадоксов Б. Рассел приводит пример с индейкой, которую кормят, за которой ухаживают, и она думает, что так будет всегда, пока не настает тот самый день, день Благодарения.
Таким образом, чтобы доказать, что все лебеди белые, мы должны проверить всех лебедей во Вселенной, и Лейбниц мне нашептывает, что это должны быть все возможные миры, что естественно невозможно. Но для того, чтобы опровергнуть это утверждение, достаточно приехать в Австралию, и встретить одного черного лебедя. Таким образом существует фундаментальная асимметрия между подтверждением и фальсификацией.
Говорить об отсутствии багов в коде, или дыр в системе в этом контексте неверно. Нельзя даже ставить вопрос в этой плоскости, потому, что это уводит дискуссию в совершенно неверном направлении, особенно если в ней задействованы люди неиспорченные матаном.
Теорема Райса накладывает отпечаток пессимизма на нашу возможность создавать совершенные системы. Следствие теоремы Райса, которая в общем виде следует из проблемы остановки машины Тюринга и вычислимости, утверждает, что не существует универсального алгоритма для доказывания или утверждения о том, что программа, система, или алгоритм не содержит ошибок и делает то, что надо. Автоматические универсальные системы тестирования в общем невозможны. В частности да, но что бы мы ни делали, — баги будут! Статическая типизация, TDD и прочие методики могут только вселить в нас больше уверенности и избавить от некоторых страхов, не более.
Существуют такие ситуации, что мы можем даже знать, что у нас существует некий специфический баг, который рушит нашу систему, потому, что мы наблюдали это в какой либо момент. Мы знаем, что баг есть. Но мы не можем его репродуцировать. Я имею в виду проблемы в мультипоточных приложениях, где правит бал недетерминизм. Нет особых проблем выловить баг, если сервер рушится каждые десять минут. Но что если нам необходимо, чтобы сервер работал несколько месяцев прежде чем проблема снова вернулась. Это в прямом смысле невозможно отладить. Хуже того, как упоминал Paul Butcher, вполне вероятно писать программы, которые содержат мультипоточные баги, которые никогда не проявятся несмотря на то, как тщательно или как долго мы бы тестировали их. Только потому, что обращения потоков к памяти могут быть переупорядочены, не означает, что так и будет сделано. И мы вполне можем быть абсолютнo в неведении о наличии проблем, пока мы не сделаем апгрейд JVM или перейдем на другое железо, где мы внезапно столкнемся с таинственными проблемами, которые никто не понимает.
Все эти три момента делают само утверждение о том, что багов нет, или о доказательстве безопасности чего либо бессмысленным. Очень большой процент ИТ профессионалов также не понимает этого. Прекрасный пример в посте Егора Бугаенко.
Если бы мне предложили на выбор две супер способности, умение делить на ноль, или находить все баги в коде, то я бы задумался, что взять, потому что это вещи одного порядка.
Существует несколько основных моментов, почему сама постановка такого типа вопросов должна быть исключена, тем более из уст ИТ профессионалов.
Первый момент — логический
Проблема индукции, которую серьезно рассмотрел Юм, ставит под сомнение саму возможность обоснования целого ряда проблем и вопросов. Например, выведение неких общих выводов из наличия неких частных наблюдений невозможно. Неограниченное количество наблюдений чего либо, не подтверждает истинность утверждения. Карл Поппер, один из невероятнейших гениев в истории человечества, обратил внимание на проблему фальсификации, и стал автором новой парадигмы в философии науки. Какова суть проблемы фальсификации и как это касается нас? Самый известный пример, — это «Черный Лебедь». Черный Лебедь был символом невозможности чего либо в 16 веке в Лондоне. Старый Мир предполагал, что все лебеди белые, поскольку все исторические записи о лебедях описывали их белые перья. И в этом контексте черные лебеди были невозможны, или не существовали. Тем не менее, в 17 веке представитель Старого Мира встретил невозможность в Австралии.
Существует асимметрия между подтверждением и фальсификацией. Проблема индукции состоит в том, что индивидуальное утверждение, как этот лебедь белый, или делая то и то, в таком то контексте, ошибки не произошло, не может быть обобщено на универсальное утверждение. Сингулярное утверждение существования не доказывает общее.
Например, если последние 4,5 миллиарда лет Солнце регулярно (хорошо — хорошо, с неким замедлением) всходило над горизонтом, то это не говорит нам, что Солнце всегда встает над горизонтом. Или любитель парадоксов Б. Рассел приводит пример с индейкой, которую кормят, за которой ухаживают, и она думает, что так будет всегда, пока не настает тот самый день, день Благодарения.
Таким образом, чтобы доказать, что все лебеди белые, мы должны проверить всех лебедей во Вселенной, и Лейбниц мне нашептывает, что это должны быть все возможные миры, что естественно невозможно. Но для того, чтобы опровергнуть это утверждение, достаточно приехать в Австралию, и встретить одного черного лебедя. Таким образом существует фундаментальная асимметрия между подтверждением и фальсификацией.
Говорить об отсутствии багов в коде, или дыр в системе в этом контексте неверно. Нельзя даже ставить вопрос в этой плоскости, потому, что это уводит дискуссию в совершенно неверном направлении, особенно если в ней задействованы люди неиспорченные матаном.
Второй момент — вычислительный
Теорема Райса накладывает отпечаток пессимизма на нашу возможность создавать совершенные системы. Следствие теоремы Райса, которая в общем виде следует из проблемы остановки машины Тюринга и вычислимости, утверждает, что не существует универсального алгоритма для доказывания или утверждения о том, что программа, система, или алгоритм не содержит ошибок и делает то, что надо. Автоматические универсальные системы тестирования в общем невозможны. В частности да, но что бы мы ни делали, — баги будут! Статическая типизация, TDD и прочие методики могут только вселить в нас больше уверенности и избавить от некоторых страхов, не более.
Третий момент — инженерный
Существуют такие ситуации, что мы можем даже знать, что у нас существует некий специфический баг, который рушит нашу систему, потому, что мы наблюдали это в какой либо момент. Мы знаем, что баг есть. Но мы не можем его репродуцировать. Я имею в виду проблемы в мультипоточных приложениях, где правит бал недетерминизм. Нет особых проблем выловить баг, если сервер рушится каждые десять минут. Но что если нам необходимо, чтобы сервер работал несколько месяцев прежде чем проблема снова вернулась. Это в прямом смысле невозможно отладить. Хуже того, как упоминал Paul Butcher, вполне вероятно писать программы, которые содержат мультипоточные баги, которые никогда не проявятся несмотря на то, как тщательно или как долго мы бы тестировали их. Только потому, что обращения потоков к памяти могут быть переупорядочены, не означает, что так и будет сделано. И мы вполне можем быть абсолютнo в неведении о наличии проблем, пока мы не сделаем апгрейд JVM или перейдем на другое железо, где мы внезапно столкнемся с таинственными проблемами, которые никто не понимает.
Все эти три момента делают само утверждение о том, что багов нет, или о доказательстве безопасности чего либо бессмысленным. Очень большой процент ИТ профессионалов также не понимает этого. Прекрасный пример в посте Егора Бугаенко.
Если бы мне предложили на выбор две супер способности, умение делить на ноль, или находить все баги в коде, то я бы задумался, что взять, потому что это вещи одного порядка.
