Питер Сейбел - Кодеры за работой. Размышления о ремесле программиста

Сейбел:А эти ребята не придут и не скажут: “Да, именно так это и есть у нас в монадах, и это разделение у нас реализовано в системе типов”?

Дойч:Знаете, я никогда не понимал монады в Haskell. Я, наверное, перестал следить за функциональными языками после ML.

Если вы посмотрите на Е - это не тот язык, о котором все знают, чтобы о нем можно было говорить, - он из тех языков, что основаны на очень четком понятии “способности”. Он связан с акторными языками Хьюитта и с операционными системами, основанными на этом понятии. В нем есть порты, или коммуникационные каналы, для обеспечения фундаментальной связи между двумя объектами. Основная идея заключается в том, что ни один из участников коммуникации не знает другого участника коммуникации. То есть это очень сильно отличается от понятия указателя, который направлен в одну сторону, и где объект, держащий указатель, достаточно хорошо представляет себе, что находится на другом конце. В нем очень важную роль играет элемент непрозрачности.

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

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

Это очень простой пример модели организации программы - если бы был способ выразить его языковыми средствами, это помогло бы людям обеспечивать соответствие кода цели, которую они для себя установили.

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

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

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

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

Сейбел:То есть, например, можно будет каким-либо образом выразить мысль “Я передаю ссылку на этот объект вот этой подсистеме, которая с ним повозится сколько-то времени, и я ничего не буду с ним делать, пока не получу его обратно”?

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