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

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

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

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

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

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

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

Кнут: Верно.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Сейбел: То есть вы замечали ошибки в своих программах и думали про себя: “Ох, я снова сделал ту же самую ошибку”.

Кнут: Да.

Сейбел: Почему же так? Может быть, дело в какой-то особой природе ошибок, что особенно затрудняет усвоение урока и недопущение подобных ошибок в будущем?

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

Сейбел: То есть теоретически вы могли бы продолжать писать системы для верстки текста до конца своей жизни?

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

Если же мы ограничиваем себя лишь тем, что действительно очень просто, то нам этого