Кодеры за работой

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

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

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

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

Кнут: Верно.

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

Кнут:

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

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

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

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

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

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

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

Сейбел:

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

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

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

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

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

Сейбел: Но разве вы не думали: «Ага, теперь, когда я увидел эту ошибку, я ее больше не повторю»?