Код есть закон? Нет, пока ещё нет.

golf-sport-e1472063337115

В этой авторской колонке Лукас Абегг рассуждает о развитии смарт-контрактов в контексте математики и утверждает, что применение таких идеалистических критериев, как «код есть закон», может серьёзно навредить развитию концепции смарт-контрактов.

Лукас Абегг – юрист, магистр права Швейцарии и США. В настоящее время он исполняет обязанности приглашённого исследователя в берлинском Университете имени Гумбольдта, где готовит докторскую диссертацию по теме «В точке пересечения права и технологий».

После провала эксперимента с ДАО разгорелась горячая дискуссия о дальнейшем пути развитии блокчейна Эфириума.

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

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

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

Давайте же взглянем на возможности смарт-контрактов внимательней.

Природа информации

Функцией смарт-контрактов, заключающей в себе самую их суть, является обработка информации.

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

Исходя из этого, следует разделить понятие «информация» на информацию синтаксическую и семантическую. Первая представляет собой правила, по которым соотносятся друг с другом символы, под второй же подразумеваются связанные с этими символами значения (т.е. «намерение»). Граница между этими двумя видами информации несколько размыта, и говорить о них отдельно друг от друга порой бывает сложно (что, как мы увидим позже, и стало первопричиной проблемы ДАО), однако очевидно, что разница между ними существует.

Интересную статью о сложности фиксации намерений написал недавно Виталик Бутерин.

Синтаксическая информация может быть подвергнута синтаксическому разбору, измерена (как это сделали в статье «Математическая теория связи» Шеннон и Уивер) и открыта для математического доказательства. Семантическая же информация – это то содержание, которое люди вкладывают в символы. Она может представлять собой всё, что угодно, о чём только может подумать человеческий мозг.

Нормализовать семантическую информацию и сделать её пригодной для машинной обработки – задача, мягко говоря, непростая. Компьютерные науки (в особенности, исследователи в области искусственного интеллекта) прилагают все силы для того, чтобы считать семантическую информацию, как, например, естественный язык, и обработать её значение программными средствами. Ситуацию осложняет ещё и то, что семантическая информация может быть какой угодно – от достаточно простой до сложной и многоуровневой.

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

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

Отсутствие регулирования

Описать различие между этими двумя типами информации можно также, разделив их на «сухой код» и «мокрый код» – эту концепцию предложил криптограф Ник Cабо.

То, почему важно помнить о двойственной природе информации, наглядно иллюстрирует история с ДАО. Императив «не навреди» (т.е. семантическая информация) был отражён только на главной странице сайта ДАО, но не в её коде (который, большей частью, оперирует исключительно синтаксической информацией).

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

Если бы существовал подходящий инструмент для работы с семантической информацией (т.е., в данном случае, обеспечивающий соблюдение всеми участниками правила «не навреди», и включающий в себя средства борьбы с нарушителями), такого разделения, вероятно, не произошло бы.

Математическое доказательство и неизменяемость

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

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

Написание кода смарт-контрактов не является значимым для развития науки действием, и можно было бы подумать, что математическое доказательство в данном случае не важно. Однако, реализуя в своём коде блокчейн и таким образом делая его неизменяемым, вы поднимаете планку для безошибочности своего кода на невероятно высокий, если не вовсе недосягаемый, уровень (для сравнения, с более подробным анализом можно ознакомиться здесь).

Поскольку ваш код не может быть впоследствии изменён, вы должны быть совершенно уверены, что он не содержит ошибок.

Поэтому представляется важным иметь математическое доказательство безошибочности вашего кода

При этом, Solidity, используемый для реализации смарт-контрактов в Эфириуме, не является языком, в котором возможно математическое доказательство (т.е. не является референциально прозрачным). Это сделало возможным включение в код семантической информации, намеренное или нет. Рекурсивный сплит, за счёт которого были выведены средства со счёта ДАО, должен был использоваться строго определённым разработчиками образом.

Очевидно, что такое намерение само по себе не могло быть зафиксировано в коде и воспрепятствовать выводу средств хакером.

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

Необходимость поддающегося проверке кода

Если ваш смарт-контракт практически целиком представляет собой неизменяемый код на основе блокчейна (как полагают единственно правильным некоторые сторонники принципа «код есть закон»), скорее всего, вы не можете обеспечить достаточный противовес в виде безошибочности вашего кода.

Всё, о чём я здесь говорю, далеко не новость.

Ещё в 2002 году Ник Cабо написал статью об использовании для контрактов формального языка, в которой прямо указал на то, что применение процедурного языка программирования может казаться заманчивым, но в реальности принесёт больше вреда, чем пользы. Это даже не говоря обо всех существующих языках программирования, применяемых в финансовой сфере, или новых способах создания языков программирования, допускающих формальную проверку (с примерами можно ознакомиться здесь и здесь).

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

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

Восполнение технических пробелов

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

Такие обходные пути могут лежать в области правовой системы реального физического мира, в частности, в области Альтернативного урегулирования споров (АУС).

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

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

Нужно только удостовериться, что каждая сторона смарт-контракта соглашается с этими правилами, подобно тому, как пользователи принимают составленные в частном порядке правила разрешения споров при регистрации доменного имени, как, например, принятый Корпорацией по управлению доменными именами и IP-адресами (ICANN) Единый порядок разрешения споров о доменных именах (UDRP).

Пример того, как может выглядеть подобная связь между смарт-контрактами и действующими в реальном мире правовыми нормами, можно найти здесь. (Это правила договорного права, а не регламент АУС, однако по реализации они очень похожи.)

Движение к исчерпывающему и однозначному пониманию законности

С первого взгляда может показаться странным использовать для перехода к новым реалиям старые концепции.

Однако если посмотреть на это как на вспомогательную конструкцию, подобно тем, какие имеются в только что напечатанных на 3D-принтере предметах и которые можно убирать, как только новый элемент прочно встаёт на своё место, то это уже не выглядит так странно. Более того, такой способ продвижения вперёд даже может нести в себе эвристический элемент – в том смысле, что это помогает больше узнать о новых концепциях и инструментах управления, которые в будущем смогут полностью заменить собой ныне существующие правовые инструменты.

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

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

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

Источник: coindesk.com

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



Рубрики:DAO, Анализ, ДАО, Мнение, смарт-контракты, эфир

Метки: , ,

4 replies

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

Trackbacks

  1. «Умные контракты» в этом сложном мире — EthereumClassic
  2. Станет ли Эфириум основой для следующего шага развития технологий? — EthereumClassic
  3. «Код есть закон» — это не закон. Часть 1 — EthereumClassic

Добавить комментарий

Заполните поля или щелкните по значку, чтобы оставить свой комментарий:

Логотип WordPress.com

Для комментария используется ваша учётная запись WordPress.com. Выход / Изменить )

Фотография Twitter

Для комментария используется ваша учётная запись Twitter. Выход / Изменить )

Фотография Facebook

Для комментария используется ваша учётная запись Facebook. Выход / Изменить )

Google+ photo

Для комментария используется ваша учётная запись Google+. Выход / Изменить )

Connecting to %s