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