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

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

Дойч: Примечательно, что я сделал точно то же самое, работая с Python. Мне как-то пришлось анализировать один очень сложный файловый формат — один из наиболее сложных музыкальных файловых форматов. Поэтому я написал в Python набор классов, которые отвечали и за парсинг, и за красивую картинку.

Связь между созданием класса и наименованием метода осуществляется в общем родителе. То есть это все делается в объектно-ориентированном стиле — макросы не требуются. Это выглядит не так красиво, как можно было бы сделать иным способом, но на выходе получается примерно так же читаемо, как и аналогичные макросы Лиспа. Есть вещи, которые на Лиспе делаются более гладко и внятно. С этим я не спорю.

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

Что касается Python, то и здесь мне приходилось делать небольшие дополнения. Это не синтаксические дополнения; это классы, примеси[70]

— многие из этих примесей дополняют то, что большинство людей привыкло считать семантикой языка. В Python за это отвечает один набор инструментов, в Лиспе — другой. Кому-то нравится одно, кому-то другое.

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

Дойч: По большому счету, я «перегорел» во время работы над Ghostscript. Ghostscript был одним из моих основных технических интересов с 1986 года, а где-то с 1992-1993 года был моим единственным крупным техническим проектом. Примерно в 1998 году я почувствовал, что сгораю, потому что не только делал всю техническую работу, но и занимался всей технической поддержкой, всеми административными вопросами. Это была компания из одного человека, и рано или поздно это должно было превысить мои возможности. Я нанял человека, чтобы создать компанию, и он стал нанимать инженеров.

После чего понадобилось еще два года, чтобы найти человека, который смог бы меня заменить. После чего потребовалось еще два года, чтобы по-настоящему передать ему все дела. К 2002 году я уже «наелся». Я уже не мог больше видеть Ghostscript.

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

Один проект, который меня одно время интересовал, был связан с моим давним приятелем по работе в Xerox, Джеем Стротером Муром, который является — или являлся — заведующим кафедры информатики в Техасском университете в Остине. Одним из его величайших достижений стало то, что он вместе с еще одним парнем из SRI по имени Боб Бойер построил просто отпадную программу по доказыванию теорем. Вокруг этой программы он создал целую группу разработчиков, построил большие библиотеки теорем и лемм по отдельным предметным областям.

И вот была эта небольшая преуспевающая группа, которая доказывала теоремы; я о них писал в своей диссертации, и мне всегда это было интересно. И они добились потрясающего результата, работая над арифметическим блоком центрального процессора AMD. И я подумал: «Хм, эта группа обладает множеством хороших качеств: они занимаются интересными мне вещами; ими управляет человек, с которым я знаком и который мне нравится; их технология базируется на Лиспе. Это действительно по мне».

Поэтому я отправился туда и прочитал там лекцию о том, как доказывание теорем могло бы — если, конечно, могло в принципе — помочь повысить уровень надежности Ghostscript. К тому времени у системы отслеживания ошибок Ghostscript была уже богатая история. Я нашел 20 ошибок, более или менее в произвольном порядке, взглянул на каждую из них и сказал: «Так, для того чтобы технологию доказывания теорем можно было бы с пользой применять для обнаружения или предотвращения этой проблемы, что должно еще произойти? Что здесь еще должно было бы появиться?»

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

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