Смарт-контракти в Tezos

Вступ до смарт-контрактів в Tezos

Що таке Michelson?

Michelson є предметно-орієнтованою мовою, яка використовується для написання смарт-контрактів в блокчейні Tezos. Michelson - мова, заснована на стеку; вона не містить змінних. Мови, орієнтовані на стеки, працюють з одним або декількома стеками, кожен з яких може бути призначений для різних цілей.
Див. Документацію Michelson і тут - серію навчальних посібників Michelson з camlCase.

Які існують високорівневі мови смарт-контрактів?

Для програмування смарт-контрактів у Tezos доступні різні високорівневі мови. Мета цих мов - полегшити процес розробки, аби Ви могли зосередитися на змісті Ваших смарт-контрактів, а не їх реалізації.
Поточні варіанти в розробці включають:
  • LIGO: Мова смарт-контрактів, що пропонує синтаксичні форми Pascal, Ocaml, і ReasonML
  • SmartPy: бібліотека Python з інструментами написання і тестування (перевірки) смарт-контрактів
  • Morley / Lorentz: eDSL з Haskell для написання смарт-контрактів

Чим високорівневі мови смарт-контрактів відрізняються від Michelson?

Високорівневі мови компілюються або інтерпретуються з метою створення дійсного Michelson. Багатьом розробникам легше працювати з мовами, оскільки вони мають простіші синтаксиси і включають такі функції, як локальні змінні і високорівневі типи, а не стекові маніпуляції.

Що таке OCaml, мова Tezos протоколу?

Протокол Tezos написаний OCaml - універсальною промисловою мовою програмування з акцентом на виразність і безпеку. Це технологія вибору компаній, в яких швидкість має вирішальне значення, а одна помилка може коштувати мільйони. Вона містить велику стандартну бібліотеку, що робить її корисною для багатьох додатків, таких як Python і Perl, і забезпечує надійні модульні і об'єктно-орієнтовані програмні конструкції, які роблять її придатною для великомасштабної розробки ПЗ. OCaml використовують багато провідних компаній, в тому числі Facebook, Bloomberg, Docker і Jane Street.

Що таке функціональне програмування? Чим воно відрізняється від інших парадигм?

Функціональне програмування (парадигма програмування) - стиль побудови структури та елементів комп'ютерних програм, який розглядає обчислення як оцінку математичних функцій і уникає змінних даних.
Це описова (декларативна) парадигма програмування, яка означає, що процес програмування виконується за допомогою виразів і оголошень замість приписів. У функціональному коді вихідне значення функції залежить тільки від аргументів, які передаються функції, так що при виконанні функції f двічі з одним і тим значенням аргументу x щоразу отримуємо однаковий результат f (x). Це відрізняється від процедур, залежних від локального або глобального стану, які можуть видавати різні результати в різний час при виклику з однаковими аргументами, але з іншим станом програми. Усунення побічних ефектів, тобто змін в стані, що не залежать від вхідних даних функції, може значно полегшити розуміння і прогнозування поведінки програми, що є одним з ключових мотивів розвитку функціонального програмування.
Дана діаграма демонструє високорівневі відмінності між EVM (Ethereum Virtual Machine), WASM (Web Assembly) і Michelson:

Мова Michelson

Вступ

Michelson - це низькорівнева мова програмування, заснована на стеку, що використовується для написання смарт-контрактів в блокчейні Tezos. Michelson було розроблено для полегшення формальної верифікації, дозволяючи користувачам підтверджувати властивості своїх контрактів. Він використовує парадигму перезапису стеку, за допомогою якої кожна функція переписує вхідний стек у вихідний. (Повне пояснення буде приведено нижче.) Це працює суто функціонально і жодною мірою не змінює вхідні дані. Таким чином, всі структури даних залишаються незмінними.

Что такое Стек?

Стек - це абстрактний тип даних, зібрання елементів з двома основними операціями: push (додає елемент до колекції) і pop (видаляє останній доданий елемент, який ще не було видалено). Порядок, в якому елементи виходять зі стеку, породжує його альтернативне ім'я, LIFO (останній увійшов, перший вийшов). Окрім того, операція перегляду може надати доступ до верхівки без зміни стеку.
Could not load image
Джерело: Wikipedia.

Переписування Стеків

Щоб зрозуміти, що означає переписувати стеки, ми проведемо транзакцію за допомогою Michelson. По-перше, перед виконанням транзакції положення блокчейна в певному хеші перетворюється і поміщається в стек як змінна storage. В нас є функція from, яка отримує дані транзакції amount, кількість прикріплених ꜩ, і parameter, параметри функції.
1
from [ (Pair (Pair amount parameter) storage) ]
Copied!
Після запуску функції, без будь-яких оновлень в стеку, програма викликає функцію to, що містить параметри result, які в свою чергу є результатом функції, і вихід storage, що перетворюється і зберігається в блокчейні.
1
to [ (Pair result storage) ]
Copied!
У цьому прикладі Michelson лише функціонально управляє стеком, а новий стек передається від функції до функції.

"Чому Michelson?" (Автор Milo Davis)

На перший погляд, Michelson здається доволі дивною мовою. Вона не включає такі функції, як поліморфізм, замикання або іменовані функції. В порівнянні з Haskell чи OCaml, вона здається недостатньо потужною. З її стеком не завжди легко розібратися, і вона не має стандартної бібліотеки. Проте, ці обмеження значною мірою пояснюються цілями розробки мови.
В Michelson є дві основні мети (мотивації):
  1. 1.
    Надати читабельний байт-код
  2. 2.
    Бути доступною для огляду
Tezos дещо відрізняється від Ethereum відносно значення смарт-контрактів. Ми розглядаємо нашу платформу як спосіб реалізації певних складових бізнес-логіки аніж загального «світового комп'ютера». В Ethereum більшість контрактів реалізують такі речі, як multisig гаманці, правила передачі і розподілу і т. д. Michelson орієнтовано на ці додатки.
Michelson розроблено як читабельну цільову платформу для компіляції, хоча її не може бути написано від руки. Мета полягає в тому, щоб зрозуміти навіть вивід компілятора. Ми розраховуємо на те, що мова буде досить простою, щоб розробники могли створювати власні інструменти аналізу і компілятори, якщо вони того забажають. Це відхід від байт-коду EVM, який більше схожий на збірку. Байт-код нижчого рівня зазвичай вимагає довіри як до Вашої програми, так і до ланцюжка інструментів компілятора. З Michelson Ви можете легко перевірити і підтвердити властивості програми, яка фактично виконується.
Використання високорівневого байт-коду також спрощує процес перевірки властивостей скомпільованого виводу. Програми, написані на Michelson, можуть бути розумно проаналізовані SMT-дозвільниками і формалізовані в Coq без необхідності застосування складніших методів, таких як логіка поділу. Так само обмеження, що накладаються примусовим відступом і капіталізацією (виділенням великими літерами), гарантують, що джерело не можна збити за допомогою прийомів з відступами і вирівнюванням.
Поточна реалізація Michelson заснована на OCaml GADT, який ми використовували для перевірки правильності мови. Крім того, реалізація мови на основі стеку відображається безпосередньо в семантиці. Те ж саме не стосується будь-якої ефективної реалізації лямбда-числення. Також відомі дві формально верифіковані реалізації Michelson: одна в Coq і одна в F *. Ми сподіваємося замінити нашу поточну реалізацію перевіреною.
Насамкінець, однією з головних переваг Tezos є те, що система може бути змінною. Ми хочемо почати з невеликої базової мови, в якій ми впевнені, і додати функції, оскільки для них створюються достойні варіанти використання. Ми не хочемо одразу перевантажувати мову, а потім порушувати зворотну сумісність.
Отже, чому Michelson? Відповідь така: для того, щоб забезпечити просту платформу для бізнес-логіки, читабельний байт-код і видимість. Коли я працював з Оліном Шиверсом, він любив говорити, що завжди потрібно використовувати «інструмент, достатньо маленький для роботи». Michelson було ретельно розроблено, щоб стати таким інструментом.

Матеріали з мов

Michelson:

Високорівневі мови смарт-контрактів:

LIGO:

SmartPy:

Morley/Lorentz:

OCaml:

Матеріали розроблені TQ Tezos перекладені українською мовою Tezos Ukraine
Last modified 1yr ago