Стил: Верно. Доказательства позволяют представить глобальную точку зрения и предусмотреть все возможности, резюмируя их при помощи очень сложной формулы. И чтобы это получить, приходится проработать кучу формул. Автор переработал статью, она снова вернулась ко мне на рецензию - и хотя я уже проделал это упражнение, пришлось опять потратить 25 часов на проверку доказательства. На этот раз, кажется, все было нормально.

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

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

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

Сейбел: И программа автоматической проверки, проверенная вручную, может сэкономить 25 часов, потраченные вами на изучение доказательства фрагмента кода?

Стил: Да. Точно.

Сейбел: О чем еще вы бы хотели поговорить?

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

Есть великолепные алгоритмы, которыми я просто восхищался. Я видел чудесные программы для сжатия кода - в те времена у тебя был всего один мегабайт памяти, и это имело значение. Было важно, сколько слов ты используешь - 40 или 30, и люди временами серьезно работали над тем, чтобы ужать программу. Билл Госпер писал эти шедевры из четырех строк, и они творили потрясающие вещи, например с усилителем, подключенным к младшим битам аккумулятора, который в это время тасовал биты.

Это может показаться бессмысленной тратой сил, но одним из лучших моментов в моей карьере был тот, когда я смог сократить программу Госпера из 11 слов до 10. И это - ценой лишь небольшого увеличения времени выполнения программы, ценой малой доли машинного цикла. Я нашел способ сократить код на одно слово, и на это у меня ушло всего лишь 20 лет.

Сейбел: И вот, спустя 20 лет, вы сказали: “Привет, Билл, а представляешь?..”

Стил: Ну, собственно, я не занимался этим все 20 лет, просто 20 лет спустя я вернулся к этой программе, и ко мне пришло озарение: я понял, что, изменив один код операции, я получу константу с плавающей запятой, близкую к тому, что мне нужно. И смогу использовать инструкцию и как инструкцию, и как константу с плавающей запятой.

Сейбел: Прямо “История Мэла, настоящего программиста”.

Стил: Точно. Я не хотел бы заниматься этим в жизни, но это был единственный раз, когда мне удалось сократить код Госпера. Это была победа. И это был красивейший кусок кода - рекурсивная подпрограмма для вычисления синусов и косинусов.

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

С IBM 1130 трудность состояла в том, что на перфокарте 12 строк, а в машинном слове было 16 бит. Так что на 16-битную инструкцию приходилось 12 бит, то есть некоторые инструкции не помещались на перфокарте. Такие инструкции приходилось собирать с помощью тех инструкций, которые помещались на перфокарте. Возникала сложная система компромиссов, какие инструкции можно использовать: если я использую вот эту инструкцию, мне нужны будут еще вот эти инструкции на перфокарте, просто чтобы собрать ее. Огромная нагрузка плюс размер функции не мог превышать 80 слов. Поэтому приходилось использовать некоторые инструкции и как данные, использовать данные повторно для других целей. Если удавалось впихнуть эту функцию в память, то ее адрес мог использоваться как константа. Такой вот стиль программирования - не то оригами, не то хайку. Я этим занимался несколько лет.

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

Стил: Они приучены работать с ограниченными ресурсами и умеют точно их оценивать.

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

Стил: Да, можно легко зациклиться на оптимизации чего только можно, даже если такая задача не стоит. Я рад, что мой сын в старшей школе освоил программирование на калькуляторах TI, где тоже были серьезные ограничения по памяти. Он научился представлять данные в сжатом виде, чтобы они подходили для калькулятора. Я не хочу, чтобы ему пришлось заниматься этим все время, но все равно опыт ценный.

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

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

Сейбел: Вы говорили о ТеХ Кнута, - она существенно больше по размерам. Что придает ей красоту?

Стил: Он взял невероятно сложную программу со множеством особых случаев и свел ее к очень простой парадигме: склеить блоки воедино. Это был важнейший прорыв. Появилось множество возможностей не только для набора текста, но и для других вещей, например для отображения на странице текста в двух измерениях. Я за то, чтобы в графических интерфейсах пользователя этот принцип склеивания блоков действовал при расположении кнопок и тому подобного.

Сейбел: Значит, здесь красота в том ощущении, что есть блок и клей, и можно сказать: “Да, это глубоко правильная идея, я проникся ее красотой и хочу видеть ее в других программах”. Вы проникаетесь ее красотой в процессе чтения кода, глядя на соотношение его элементов? Или же, прочитав код, говорите: “Великолепно, все основано на этой простой, но не упрощенной идее”?

Стил: И то и другое. Кнут замечательно умеет рассказывать о коде. Можно целый день читать “Искусство программирования”, погружаться в алгоритмы. Он объясняет вам их, показывает, как их можно использовать, дает упражнения, и создается ощущение, что вас увлекают в интересное путешествие. И попутно показывают вам очень занятные вещи. Если пробираться через код ТеХ, ощущения сходные. Я много чего понял о программировании. Одни куски кода вполне обычны, порой даже поверхностны. А при виде других говоришь себе: “Даже не подозревал, что можно сделать так”. Есть и то, и то.

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

Стил: Да. В комитете по разработке Common Lisp мы часами обсуждали конец строки, чтобы добиться совместимости с UNIX, где есть только символ перевода строки, и с системами PDP-10, где используется CR LF. Надо было приспособить перевод строки для обоих систем. Настоящий кошмар.