Семантические смарт-контракты и управление инвестициями
Пресуппозиция
- В статье (https://m.facebook.com/story.php?story_fbid=10209885634250092&id=1610666320) упоминается CFSD — Crypto Fund Syndication Protocol. Как я понимаю, речь идет о протоколе для совместного финансирования тех или иных проектов, что позволяет фондам в автоматическом или полуавтоматическом режиме делать совместные инвестиции для снижения своих рисков и распределения этих рисков между несколькими участниками инвестирования.
- У инвесторов вообще есть проблема верификации и аудита тех проектов, куда они инвестируют. Верификация в случае крипто проектов на основе смарт-контрактов означает проверку на соответствие того, что написано в смарт-контракте, тому, что написано в white paper и бумажных договорах (если такие есть) между инвестором и проектом. Аудит же — это проверка на соответствие того, как реально работает смарт-контракт, тем бумажным обязательствам, которые на себя взял проект перед инвесторами.
Комментарий
Верификация и аудит крипто-проектов
Проблема верификации и аудита проектов для крипто-фондов более актуальна, чем для частных инвесторов, которые отвечают каждый за себя. Это связано с тем, что пайщики перекладывают проблему оценки проекта на фонд. И тот несет ответственность перед каждым своим инвестором.
И в конкурентной борьбе преимущество будет у того фонда, который не только обещает лучшую доходность, но и лучше оценивает проект, риски. Который сможет контролировать проект на всех стадиях его развития.
Поскольку мы говорим о специфичной области крипто-проектов, то здесь не обойтись без технических инструментов контроля. Стандартным подходом является использование смарт-контрактов. Первые идеи смарт-контрактов были предложены в 1994 году Ником Сабо (англ. Nick Szabo). Некоторые принципы смарт-контрактов были заложены в протоколе первой блокчейн-валюты Bitcoin, однако они не были реализованы в клиентском ПО, не обладали полнотой по Тьюрингу из соображений безопасности и не использовались на практике. Смарт-контракты впервые начали применяться в проекте Ethereum.
Сейчас смарт-контракты применяются узкоспециализированно: в основном на этапе выпуска токенов и выполнения транзакций. Однако, с помощью них возможно полностью или частично автоматизировать задачи верификации и аудита проектов. Например, формировать отчеты о финансовых показателях, контролировать условия сделки, условия распределения инвестиционных средств и т.п.
Те фонды, которые смогут автоматизировать задачи верификации и аудита, смогут не просто управлять более крупными инвестиционными портфелями и проектами, но будут делать это более качественно.
Выбор языка для смарт-контрактов
Верификация проектов на основе смарт-контрактов является серьезной проблемой, в случае использования процедурных и функциональных языков программирования (то, что принято называть «полных по Тьюрингу»).
Проблема проистекает из известной теоремы Гёделя о неполноте, которая в применении к теории алгоритмов говорит о том, что невозможно создать такую программу, которая сможет предсказать поведение другой программы.
Иными словами, языки программирования смарт-контрактов могут оказаться слишком сложными и запутанными. Это подтверждает практика Ethereum. Известны случаи, когда в результате ошибок в смарт-контрактах, проекты и транзакции срабатывали не так, как было запланировано. Были обнаружены ошибки в виртуальной машине EVM для языка Solidity. Из-за сложности языка в Ethereum применяется система стороннего аудита смарт-контрактов, когда некие эксперты анализируют код, а потом выносят вердикт — этот смарт-контракт похож на то, что обещает проект.
Такая практика далека от того, что хотели бы крипто-фонды, обычные крипто-инвесторы и все крипто-сообщество. В идеале, код смарт-контракта должен был понятен обычному человеку и должен допускать автоматическую проверку, еще до стадии исполнения.
Мы предлагаем решать проблему верификации на концептуальном уровне.
А именно, стоит выбрать такой класс языков для смарт-контрактов, для которых можно полностью или частично автоматизировать проблему верификации. А если что-то невозможно верифицировать автоматически, то можно было бы решить с помощью человека (с предсказуемым временем решения и временем обучения персонала).
Для этой цели предлагается использовать теорию исполнимых спецификаций (или другое название — теория семантического программирования/моделирования), разработанную в ИМ СО РАН еще в 80–90-х годах ак. Ершовым Ю.Л., ак. Гончаровым С.С., и ак. Свириденко Д.И.
Они описали, как строить классы языков программирования на основе конструктивной логики предикатов первого порядка, которые с одной стороны будут близки к языку той или иной проблемной области, и таким образом понятны специалистам, а с другой стороны будут не просто исполнимы, но и для них можно построить эффективную исполнимую семантику (в смысле автоматической трансляции в алгоритм исполнения).
