Кодеры за работой. Размышления о ремесле программиста - [227]

Кнут: С одной стороны, невозможно что-либо доказать в принципе. Когда кто-то говорит, что его программа верифицирована, это значит, что она лишь соответствует неким критериям согласно результатам работы верификатора. Но в верификаторе может быть ошибка. Критерии могут быть неправильно сформулированы. Никогда нельзя с точностью утверждать, что программа корректна. У вас может быть достаточно причин, чтобы в это верить, но при этом вы никогда не добираетесь до конца цикла. Это теоретически невозможно.

Самая первая работа Тони Хоара про формальное доказательство называлась “Proof of a Program: FIND (Доказательство программы: FIND). Это было прекрасное научное исследование, которое весьма продвинуло общее положение дел в этой области. Но в этом доказательстве было 2-3 ошибки. Тогда людям не приходило в голову проверять, находится ли список индексов внутри границ или еще что-нибудь в этом духе. Всегда есть опасность появления пробелов. Тем не менее он осуществил гораздо более качественную и тщательную проверку, чем кто-либо до него.

Или вот вчера я закончил программу и понятия не имею, как установить для нее все операторы утверждений. Мне это никогда не сделать, потому что я никогда не буду больше уверен в утверждениях, нежели в самой программе.

Или взять, к примеру, ТеХ - с формальной точки зрения там полный бардак. Задумывалось, что эту программу будут использовать люди, а не компьютеры. Было бы абсолютно невозможно сформулировать, что значит корректность для ТеХ. Некоторые методы формальной семантики настолько сложны, что никто не может внятно определить понятие корректности.

Сейбел: Работая над ТеХ, вы написали совершенно зубодробительный тест для программы.

Кнут: Верно.

Сейбел: Каким образом вам удается так относиться к своим программам? Программисты зачастую хотят защитить свое дитя, поэтому они, как правило, стараются не очень усердно тестировать свои программы.

Кнут: Я всю жизнь был придирчивым. И чтобы получить удовольствие от обнаружения ошибок, мне нужно просто забыть, что программу написал я сам. Я пытаюсь представить, что это чья-то чужая программа. В остальных же случаях мне достаточно легко переключиться в режим нападения. Не знаю почему.

Например, одно из моих лучших профессиональных достижений во время работы в Burroughs Corporation было связано с деятельностью по обнаружению ошибок в устройстве их аппаратного обеспечения. Их инженеры показывали мне спецификации для своих компьютеров, а мне нужно было сконструировать примеры, при которых они бы ошибались на единицу или что-то вроде того. Я нашел свыше 200 ошибок в их компьютерах серии В-5000, прежде чем они поступили в производство, хотя перед этим они прошли тест на эмуляторах.

Сейбел: То есть, по сути, вы изобретали программы, которые были верны с точки зрения семантики языка, но машина исполняла их некорректно?

Кнут: Да. Конечно же, если у них плавающая запятая неправильно вычисляла произведение двух чисел, я пытался найти примеры чисел, когда плавающая запятая не работала. Кроме того, иногда они реали-зовывали стек аппаратно, и у них были ситуации, когда регистры были пусты или не на верху стека, и я пытался придумать сценарии, в которых их логика не работала.

Сейбел: Вы делали это по какой-то системе? Как вы находили все эти вещи?

Кнут: Может быть, я просто излишне придирчив? Не знаю. Но если я пытаюсь что-то доказать, например теорему, если речь о математике, а не доказать правоту чего-либо, то мне, как правило, проще сказать: “Давайте найдем контрпример”. Я могу просто завестись, отыскивая дырку во всем этом или пытаясь объяснить, почему это не работает. Если же не могу найти никаких дырок, то вижу доказательство.

Думаю, все дело во мне - я люблю придираться и отыскивать ошибки. Мне гораздо интереснее, когда я выступаю против чего-либо, а не просто сижу и приговариваю: “Ага, да, это работает. Интересно, почему?”

Сейбел: Любопытно, что именно это движет вас вперед, хотя всю свою жизнь вы посвятили объяснению проблем. Не думаете ли вы, что такой подход подпитывает ваше стремление все объяснять?

Кнут: Единственное, что можно утверждать по поводу моих объяснений, - я пытаюсь совместить в естественном мыслительном процессе наблюдения за явлениями одновременно два разных способа, чтобы понять что-либо лучше. Думаю, чрезвычайно важно видеть вещи объемно, а не в одном измерении. Не знаю, как это связано с моей придирчивостью.

Но когда нападаешь, пытаясь кого-то победить, как в игре, это пробуждает соревновательный дух, что-то такое, что стимулирует мой мозг, так что я пытаюсь решить поставленную передо мной задачу более чем одним способом. С хорошим объяснением дело обстоит так же. В хорошем объяснении каким-то образом сочетаются разные точки зрения.

Сейбел: Еще один вывод, который вы вынесли из работы над ТеХ - вы об этом писали в “The Errors of ТеХ” (Ошибки ТеХ), - нужно фиксировать каждую ошибку, обнаруженную в программе. Ребята вроде сотрудников Института разработки ПО считают, что процесс разработки ПО можно назвать взвешенным и зрелым, если вы отслеживаете все ваши ошибки и пытаетесь понять, как предотвратить подобные ошибки в будущем. Но вы говорили о том, что ведение журнала ошибок никоим образом не помогает вам предотвращать появление ошибок в будущем.