C’est en Michelson que les smart-contrats sont programmés dans Tezos. Dans cet article nous allons voir ce qu’est Michelson, et les raisons qui ont motivé le choix de ce langage pour Tezos.

Michelson

Michelson est un langage stack based, avec des types de données, des primitives de haut niveau et une vérification de type statique stricte. Il présente quelques ressemblances avec d’autres langages. Les connaisseurs remarqueront des références directes à Forth, Scheme, ML et Cat.

Un programme en Michelson est une série d’instructions qui sont exécutées en séquence : chaque instruction reçoit en entrée le stack résultant de l’instruction précédente et la réécrit pour la suivante. Le stack contient à la fois des valeurs immédiates et des structures allouées au tas. Toutes les valeurs sont immuables et la mémoire inutilisée est recyclée.

Ainsi, un programme en Michelson reçoit en entrée un stack d’éléments uniques, contenant une valeur d’entrée et le contenu d’un espace de stockage. Il doit renvoyer un stack d’éléments unique contenant une valeur en sortie, une liste des opérations internes et le nouveau contenu de l’espace de stockage. Sinon, un programme de Michelson peut échouer, en utilisant explicitement un code d’opération spécifique ou en raison d’une erreur qui ne pourrait pas être interceptée par le système de types (par exemple, division par zéro ou épuisement des gas).

Les types d’entrée, de sortie et de stockage sont fixes et monomorphes, et le programme est vérifié avant d’être introduit dans le système. Aucune exécution de smart-contract ne peut échouer car une instruction a été exécutée sur un stack de longueur ou de contenu inattendu.

Un language adapté pour Tezos

À première vue, Michelson est un langage spécifique. En effet, il n’offre pas les fonctionnalités classiques telles que le Polymorphisme, les Closures, ou même les fonctions nommées. Comparé aux langages tels que Haskell (utilisé pour programmer le core de Cardano) ou OCaml (utilisé pour programmer le core de Tezos), Michelson semble moins puissant. Son stack n’est pas toujours facile à gérer et il ne dispose pas de bibliothèque standard. Mais ces restrictions sont largement motivées par les objectifs de la conception de ce langage.

Tezos a une vision un peu différente de celle d’Ethereum concernant les smart-contracts. Tezos est d’avantage un moyen d’implémenter des éléments répondant à une logique métier, qu’un « ordinateur mondial » générique. Dans Ethereum, la plupart des contrats implémentent des éléments tels que les wallets multisig, les règles d’acquisition et de distribution, etc. Michelson est ciblé sur ces applications, et non sur des programmes arbitraires.

Michelson est conçu comme une « cible de compilation lisible ». En ce sens, l’objectif est que même l’output d’un compilateur puisse être compris. Le langage doit être suffisamment simple pour que les développeurs puissent construire, s’ils le préfèrent, leurs propres outils d’analyses et leurs propres compilateurs.

C’est différent par rapport au bytecode de l’EVM (Ethereum Virtual Machine), qui ressemble plus à l’assemblage. Avec un bytecode de niveau inférieur, il faut avoir confiance à la fois dans le programme et dans la chaîne d’outils du compilateur. Avec Michelson, vous pouvez plus facilement vérifier les propriétés du programme qui est réellement exécuté. L’utilisation d’un bytecode de niveau supérieur simplifie également le processus de vérification des propriétés concernant l’output compilé. Les programmes écrits en Michelson peuvent être raisonnablement analysés par les solveurs SMT et formalisés en Coq sans recourir à des techniques plus complexes, telles que la logique de séparation. De même, les restrictions imposées par l’indentation forcée empêchent que la source soit illisible à cause de problèmes d’indentation et d’alignement.

Pour Tezos, l’implémentation actuelle de Michelson est basée sur un OCaml GADT, utilisé pour vérifier la validité typographique de la langue. De plus, l’implémentation d’un stack de langage mappe directement à la sémantique. Il n’en va pas de même pour une mise en œuvre efficace du lambda-calcul. Il y a eu deux implémentations officiellement vérifiées de Michelson, une en Coq et une en F *.

Enfin, l’un des principaux avantages de Tezos est que le système est modifiable. L’idée est de commencer avec un langage de base avec lequel il est possible d’ajouter des fonctionnalités. Plutôt que trop s’appuyer sur le langage complexe, et risquer des problèmes de compatibilités lors de modifications.

Alors, pourquoi Michelson ? Fournir une plate-forme simple pour la logique métier, fournir un bytecode lisible et être introspectable.

Sources :

tezos.gitlab.io

michelson-lang.com


0 commentaire

Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée. Les champs obligatoires sont indiqués avec *