Michelson
Michelson is the domain-specific language used to write smart contracts on the Tezos blockchain. Users can write Michelson directly, but most of them use a high-level language for a more approachable syntax and for more user-friendly programming features; see Languages.
Features
Michelson is a Turing-complete stack-based language that includes common features of a programming language as well as some specific blockchain-related features:
- It doesn't have variables but instead manipulates data directly on a stack, through a set of stack manipulation instructions. For example, the
ADDinstruction consumes two elements from the top of the stack and puts their sum on top of the stack. - It is strongly typed, with basic types such as integers, amounts of tez, strings, and account addresses, as well as complex types such as pairs, lists, key-value stores (big-maps), or pieces of code (lambdas).
- It has limited access to data, and can only read data from its own storage, data passed as parameters during calls to its entrypoints, and a few special values such as the balance of the contract, the amount of tez sent to it during a call, and the creation time of the current block. It can also access a table of constants.
Michelson was designed to facilitate formal verification, allowing users to prove the properties of their contracts.
Michelson uses a stack rewriting paradigm, whereby each function rewrites an input stack into an output stack. (The meaning of this will be fully explained below.) This runs in a purely functional way and does not modify the inputs at all. Thus, all data structures are immutable.
What is a stack?
A stack is an abstract data type that serves as a collection of elements, with two principal operations: push (adds an element to the collection) and pop (removes the most recently added element that has not yet been removed). The order in which elements come off a stack gives rise to its alternative name, LIFO (last in, first out). Additionally, a peek operation may give access to the top without modifying the stack.
Source: Hyperthermia on Wikimedia Commons.
Rewriting Stacks
To see what mean it means to rewrite stacks, we will run through a transaction in Michelson. First, before a transaction runs, the blockchain state at a certain hash is deserialized and put onto the stack as the variable storage. We have a from function that receives the transaction data amount, the amount of attached tez, and the parameter, the function's parameters.
from [ (Pair (Pair amount parameter) storage) ]
After running the function, without any updates to the stack, the program will call a to function that has the parameters result, which is the result of the function, and the output storage that is serialized and stored on the blockchain.
to [ (Pair result storage) ]
In the example, Michelson only manipulates the stack functionally and a new stack is passed from function to function.
Entrypoints
Depending on the high-level language used, a smart contract deployment also defines its entrypoints using the complex Parameter Type. These are special functions used to dispatch invocations of the smart contract. Each entrypoint is in charge of triggering an instruction. Below is the same example as before, abstracting the complex Parameter Type:
Each type and position of a parameter in the list (or pair) allows you to define an entrypoint (a function). For instance, in our example, there are two parameters, hence two types. Both types are integers (to increase or decrease a value). Because the type is the same, its position (left, right, or index number) determines which entrypoint is correct. It could be:
- Left type: "Increment" entrypoint
- Right type: "Decrement" entrypoint
Below is another illustration of this process:
For more information, see Entrypoints.