Я все это говорю, чтобы показать, что использую крайне примитивные техники отладки, например через небезопасные операторы printf. Тут нечем гордиться. Но долгое время ничего больше не было — по крайней мере, если брать GHC. Я выработал способы, которые делают для меня этот путь самым коротким.

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

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

Возможно, вы разговаривали в основном с людьми академического склада и с теми, кто в силу возраста не привык к сложным отладчикам. Я бы не стал делать никаких общих выводов. И, конечно, не хочу принизить значение качественных отладчиков — особенно для сложных систем с множеством программных слоев. GHC очень прост сравнительно со средой .NET, где есть слои DOM и UML, и не знаю, что еще. Теперь вокруг столько примочек, что программная поддержка становится действительно важной.

Сейбел: Еще один способ создавать правильные программы — формальные доказательства. Что вы думаете об их полезности?

Пейтон-Джонс: Представьте, что ваша цель — иметь для всего автоматическую проверку правильности. Что это будет означать? Проверка по сравнению с чем? По сравнению с некоей спецификацией. Что за спецификация? Она должна описывать все, что делает программа, иначе проверка невозможна. Итак, должна быть формальная спецификация для каждого действия программы. Как написать такую спецификацию? Допустим, вы пользуетесь функциональным языком. Тогда, может быть, ваша спецификация — это и есть ваша программа?

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

Более продуктивным для практических целей будет описание некоторых свойств, которыми должна обладать программа. К примеру, вы пишете: «Клапан 1 никогда не должен закрываться одновременно с клапаном 2. Это дерево всегда должно быть сбалансировано. Эта функция всегда должна иметь результат больше нуля». Это небольшие частичные спецификации, не полные. Это просто утверждения, в которых вы хотите быть уверены.

Как их написать? Функциональные языки неплохо приспособлены для этого. Именно это и происходит, если писать спецификацию в Quick-Check — свойства получаются функциями языка Haskell. Допустим, мы хотим проверить, что функция reverse является своей противоположностью, тогда мы напишем check reverse с типом список из А -> булевское значение. Итак, checkreverse от xs будет: reverse от reverse xs равно xs. Это функция, которая всегда оказывается верной. Функция-свойство. Но она написана на том же самом языке, и это здорово.

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

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

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

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

Мне кажется очень важным уйти от этого глобального подхода, «все или ничего», в сторону очень полезного статического и динамического тестирования частичных спецификаций. Это повысит вашу уверенность в правильности программы, а на большее рассчитывать нельзя. Даже так называемые полные спецификации не учитывают вещи вроде того, что программа должна работать за 0,1 с или занимать не более 10 Кбайт памяти. Часто в них ничего не говорится о ресурсах, о времени. Даже если программа формально отвечает спецификации, из-за этих мелочей она может работать не так, как нужно. Думаю, мы обманываем себя, когда говорим, что проверили программу и все в порядке. Лучше честно сказать, что мы повышаем свою уверенность в ней. Тут все может начинаться скромно — вы повышаете уверенность на 75%, прикладывая всего 5% от общего количества усилий. Это хороший показатель.

Сейбел: Поговорим о параллелизме. Гай Стил поручил мне задать вам вопрос о транзакционной памяти — спасет она мир или все же нет?

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

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