Смарт-контракты в Tezos
Michelson является предметно-ориентированным (специфическим) языком, используемым для написания смарт-контрактов в блокчейне Tezos. Michelson - язык, основанный на стеке; в нем нет переменных. Языки, ориентированные на стеки, работают с одним или несколькими стеками, каждый из которых может быть предназначен для разных целей.См. документацию Michelson и здесь - серию учебных пособий Michelson по camlCase.
Для программирования смарт-контрактов для Tezos доступны различные высокоуровневые языки. Цель этих языков - облегчить процесс разработки, чтобы Вы могли сосредоточиться на содержании Ваших смарт-контрактов, а не на их реализации.
Текущие варианты в разработке включают:
LIGO: Язык смарт-контрактов, предлагающий синтаксические формы Pascal, Ocaml, и ReasonML
SmartPy: библиотека Python с инструментами написания и тестирования (проверки) смарт-контрактов
Morley/Lorentz: eDSL с Haskell для написания смарт-контрактов
Высокоуровневые языки компилируются или интерпретируются с целью создания действительного Michelson. Многим разработчикам легче работать с языками, так как они имеют более простые синтаксисы и включают в себя такие функции, как локальные переменные и высокоуровневые типы, а не стековые манипуляции.
Протокол Tezos написан на OCaml, универсальном промышленном языке программирования с упором на выразительность и безопасность. Это технология выбора компаний, в которых скорость имеет решающее значение, а одна ошибка может стоить миллионы. У него большая стандартная библиотека, что делает его полезным для многих приложений, таких как Python и Perl, и обеспечивает надежные модульные и объектно-ориентированные программные конструкции, которые делают его применимым в крупномасштабной разработке ПО. OCaml используют многие ведущие компании, в том числе Facebook, Bloomberg, Docker и Jane Street.
Функциональное программирование (парадигма программирования) - стиль построения структуры и элементов компьютерных программ, который рассматривает вычисления как оценку математических функций и избегает изменяющихся переменных данных.
Это описательна (декларативная) парадигма программирования, которая означает, что программирование выполняется с помощью выражений или объявлений вместо предписаний. В функциональном коде выходное значение функции зависит только от аргументов, которые передаются функции, так что при вызове функции f дважды с одним и тем же значением аргумента x каждый раз получается один и тот же результат f (x). Это отличается от процедур, которые зависят от локального или глобального состояния, которые могут давать разные результаты в разное время при вызове с одинаковыми аргументами, но с другим состоянием программы. Устранение побочных эффектов, т.е. изменений в состоянии, которые не зависят от входных данных функции, может значительно облегчить понимание и прогнозирование поведения программы, что является одним из ключевых мотивов развития функционального программирования.
Данная диаграмма демонстрирует высокоуровневые различия между EVM (Ethereum Virtual Machine), WASM (Web Assembly) и Michelson:
Michelson - это низкоуровневый язык программирования, основанный на стеке, который используется для написания смарт-контрактов в блокчейне Tezos. Michelson был разработан для облегчения процесса формальной верификации, позволяя пользователям подтверждать свойства своих контрактов. Он использует парадигму перезаписи стека, посредством которой каждая функция переписывает входной стек в выходной. (Полное объяснение будет приведено ниже.) Это работает чисто функционально и ни в коей мере не изменяет входные данные. Таким образом, все структуры данных остаются неизменными.
Стек - это абстрактный тип данных, являющийся собранием элементов с двумя основными операциями: push (добавляет элемент в коллекцию) и pop (удаляет последний добавленный элемент, который еще не был удален). Порядок, в котором элементы выходят из стека, порождает его альтернативное имя, LIFO (последний вошел, первый вышел). Кроме того, операция просмотра может предоставить доступ к верхушке без изменения стека.
Источник: Wikipedia.
Чтобы понять, что значит переписывать стеки, мы проведем транзакцию используя Michelson. Во-первых, перед выполнением транзакции положение блокчейна в определенном хеше преобразуется и помещается в стек как переменная storage. У нас есть функция from , которая получает данные транзакции amount , количество прикрепленных ꜩ, и parameter , параметры функции.
from [ (Pair (Pair amount parameter) storage) ]
После запуска функции, без каких-либо обновлений в стеке, программа вызывает функцию to, содержащую параметры result, которые являются результатом функции, и выход storage, который преобразуется и хранится в блокчейне.
to [ (Pair result storage) ]
В этом примере Michelson лишь функционально управляет стеком, а новый стек передается от функции к функции.
На первый взгляд, Michelson кажется довольно странным языком. Он не предусматривает такие функции, как полиморфизм, замыкания или именованные функции. В сравнении с Haskell или OCaml, он кажется недостаточно мощным. С его стеком не всегда легко разобраться, и нет стандартной библиотеки. Однако эти ограничения в значительной степени объясняются целями разработки языка.
У Michelson есть две основные цели (мотивации):
Предоставить читаемый байт-код
Быть обозримым
Tezos несколько отличается от Ethereum в отношении значения смарт-контрактов. Мы рассматриваем нашу платформу в качестве способа реализации определенных составляющих бизнес-логики нежели общего «мирового компьютера». В Ethereum большинство контрактов реализуют такие вещи, как multisig кошельки, правила передачи и распределения и т. д. Michelson нацелен на эти приложения.
Michelson разработан как читаемая целевая платформа для компиляции, хотя он может быть написан от руки. Цель состоит в том, чтобы понять даже вывод компилятора. Мы рассчитываем на то, что язык будет достаточно простым, чтобы разработчики могли создавать свои собственные инструменты анализа и компиляторы, если они того пожелают. Это отход от байт-кода EVM, который больше похож на сборку. Байт-код более низкого уровня обычно требует доверия как к Вашей программе, так и к цепочке инструментов компилятора. С Michelson Вы можете легко проверить и подтвердить свойства программы, которая фактически выполняется.
Использование высокоуровневого байт-кода также упрощает процесс проверки свойств скомпилированного вывода. Программы, написанные на Michelson, могут быть разумно проанализированы SMT-разрешителями и формализованы в Coq без необходимости применения более сложных методов, таких как логика разделения. Точно так же ограничения, накладываемые принудительным отступом и капитализацией (выделением заглавными буквами), гарантируют, что источник не может быть сбит с помощью приемов с отступами и выравниванием.
Текущая реализация Michelson основана на OCaml GADT, который мы использовали для проверки правильности языка. Кроме того, реализация языка на основе стека отображается непосредственно в семантике. То же самое не относится к любой эффективной реализации лямбда-исчисления. Также известны две формально верифицированные реализации Michelson: одна в Coq и одна в F *. Однажды мы надеемся заменить нашу текущую реализацию проверенной.
В заключение, одно из главных преимуществ Tezos заключается в том, что система может быть изменяемой. Мы хотим начать с небольшого базового языка, в котором мы уверены и добавить функции, поскольку для них создаются достойные варианты использования. Мы не хотим сразу перегружать язык, а затем нарушать обратную совместимость.
Итак, почему Michelson? Ответ таков: для того, чтобы обеспечить простую платформу для бизнес-логики, читаемый байт-код и обозримость. Когда я работал с Олином Шиверсом, он очень любил говорить, что всегда нужно использовать «инструмент, достаточно маленький для работы». Michelson был тщательно разработан, чтобы быть этим инструментом.
LIGO IDE
Материалы разработаны TQ Tezos переведены на русский язык Tezos Ukraine
