# A Tutorial Introduction to Michelson & Tezos, Part I: Hello Michelson

Michelson is the smart contract language of the Tezos blockchain. Roughly speaking, Michelson is to Tezos as the Ethereum Virtual Machine is to Ethereum. Both languages are stack-based, which means that computation is performed by mutating a sequence of data elements (the stack) according to some sequence of instructions (the program).

The most notable difference between Michelson and EVM is that Michelson is written in a human-legible text format, whereas EVM operations are represented as bytes. For example, if you look up the opcode table for the EVM you’ll see that the opcode `01` takes two numbers (off the top of the stack) and adds them together. The equivalent operation in Michelson is written as `ADD`.

(To be fair, the addition opcode `01` in the EVM has `ADD` as an intermediate mnemonic representation)

In the above image, we have a stack that we can write out as

``20 : 7 : 13 : 45 : []``

where `:` is our element separator and `[]` indicates the bottom of the stack.

In the illustration we apply the operation `ADD` to the stack, which has the following definition:

``ADD / a : b : S => (a + b) : S``

In plain English, this definition says “The `ADD` operation removes the top two elements of the stack (`a` and `b` in the definition) and then puts the element `(a + b)` back onto the top of the stack:

``ADD / 20 : 7 : 13 : 45 : [] =>  (20 + 7) : 13 : 45 : [] =>  27 : 13 : 45 : []``

All computation with Michelson works similarly based on this process of stack mutation. We used `ADD` in the above example, but we could also mutate the stack with other arithmetic operations like subtraction or multiplication, or logical operations like `NOT`, `AND`, `OR`. We can directly manipulate the stack by explicitly pushing data onto it, or by swapping around or duplicating elements. We have control flow structures like `LOOP` or `IF`. We can perform some cryptographic operations like hashing or checking signatures, and we can interact with the blockchain by initiating token transfers or creating accounts. Michelson has lot of different operations.

The second major difference between Michelson and EVM, is that Michelson data elements are typed.

Broadly speaking, a type is a piece of information that constrains the possible things that can be done with a given data value.

If the value `1` has the type `int` (for integer), then we know that we can safely perform numerical addition on it, but that we can't safely perform list indexing.

For the value `"foobar"` with type `string`, the situation is reversed. Adding a number to a list `1 + "foobar"` is not well-defined, because addition is an operation on integers (in most languages, some languages overload the `+` operator to mean numerical addition when its arguments are numbers and concatenation when its arguments are strings)

Types are useful because they allow the Michelson interpreter to exclude programs that may have problematic behaviour. For example, with the natural number type, `nat`, attempting to subtract a larger `nat` from a smaller `nat` like `4 - 5` will result in an error. The programmer then can determine during testing whether this error is the result of an undesired operation, incorrect arguments, or whether the type signature of the values ought to be changed. The crucial thing is that this error occurred early on and prevented the program from running at all, rather than for the possible bug to slip past testing unnoticed only to cause issues later on in production.

Generally speaking, types allow the programmer to communicate their intentions in more detail to the machine, and allows the machine to communicate to the programmer when execution deviates from those intentions.

Okay, now that we’ve covered a little bit of the theory of how Michelson works, let’s get our hands dirty with some code.

The easiest way to play with Michelson is to install the Tezos client from using docker. In your terminal type the following commands:

``\$ wget https://gitlab.com/tezos/tezos/raw/alphanet/scripts/alphanet.sh``
``\$ chmod +x ./alphanet.sh``
``\$ ./alphanet.sh start``

This should spit out a bunch of output that you can mostly ignore for now. The important thing is that packaged within the Tezos client is a Michelson runtime we can use to test our programs.

Alternatively, you can build Tezos from source by following the instructions in the Tezos Docs

Open up your favorite editor and write the following program `helloTezos.tz` in the same directory you put the `alphanet.sh` script.

``# helloTezos.tzparameter unit; storage string; code {DROP;  PUSH string "Hello Tezos!";  NIL operation; PAIR;};``

First we’re going to check that the script is well-typed:

``\$ ./alphanet.sh client typecheck script container:helloTezos.tz``

We can see more information emitted by the typechecker by adding the `--details` flag:

``\$ ./alphanet.sh client typecheck script container:helloTezos.tz --details``

This program should typecheck, but if it doesn’t, possible reasons are if the file was copied incorrectly, or if there have been breaking changes to the Michelson semantics since this document was published.

Now that we know the program typechecks, we’re going to run it. The command for telling the tezos client to run a Michelson program (in a sandbox) is:

``\$ ./alphanet.sh client run script <path> on storage <data> and input <data>``

where `<path>` is the path to the program source (since we're using docker this will be prepended with `container:`), and `<data>` is some Michelson value.

We’ll go over what `storage` and `input` mean below. For now, try running:

``\$ ./alphanet.sh client run script container:helloTezos.tz on storage '""' and input Unit``

This should return:

``storage "Hello Tezos!" emitted operations``

Congratulations, you’ve just run your first smart contract in Michelson!

Now let’s get into the details of how the contract works:

All Michelson smart contracts are functions that take two arguments, an input parameter and a storage value, and return a pair of a list of operations and a storage value. The storage value is effectively a return value, and the list of operations are like a continuation, if, for example, the contract was called by another contract.

There are many different ways to notate types signatures but here’s what the Michelson type signature of a contract looks like:

``lambda (pair 'parameter 'storage) (pair (list operation) 'storage)``

Personally, I prefer type notation more like Haskell’s, but both signatures are equivalent:

``contract :: (Parameter p, Storage s) -> ([Operation], Storage s)``

Let’s take another look at `helloTezos.tz`:

``# helloTezos.tzparameter unit; storage string; code {DROP;  PUSH string "Hello Tezos!";  NIL operation; PAIR;};``

The `parameter unit` and `storage string` lines specify the types of the contract's two arguments. If we concretize the above signature for the general type of Michelson contracts, with `'parameter` as `unit` and `'storage` as `string`, we get the type of our specific `helloTezos.tz` contract:

``lambda (pair unit string) (pair (list operation) string)``

The initial stack of a Michelson contract is its argument pair `(pair 'parameter 'storage)` so `helloTezos.tz` starts with a stack of type:

``:: (pair unit string) : []``

At the command line we ran

``\$ ./alphanet.sh client run script container:helloTezos.tz on storage '""' and input Unit``

`'""'` is the command-line syntax for `""`, the empty string and `Unit` is the data constructor of the single inhabitant of the `unit` type. Be advised that input and parameter are synonymous here. So our initial stack has the concrete value:

``(Pair Unit "") : []``

which has type

``:: (pair unit string) : []``

The distinction between `Pair` and `pair` is that `Pair` is a data constructor and `pair` is a type. Data constructors in Michelson begin with an initial capital, whereas types are all lowercase.

Now we have our initial value, and our return type, we can think about the the execution of our contract as a sequence of operations that transform our initial value into a return value that matches our return type.

In other words, we started with

``(Pair Unit "") : [] :: (pair unit string) : []``

and we want to end up with

``??? :: (pair (list operation) string) : []``

Fortunately, our contract is pretty short at only 4 operations, so we can walk through the steps of this transformation here. The operations are written after the `code` heading in `helloTezos.tz`:

``# helloTezos.tz code {DROP;  PUSH string "Hello Tezos!";  NIL operation; PAIR;};``

If we write down this operation sequence and the initial values and types from the previous section, we get the full state of our Michelson stack machine:

``STATE code DROP; PUSH string "Hello Tezos!"; NIL operation; PAIR; stack (Pair Unit "") : [] type :: (pair unit string) : []``

The `DROP` operation removes (or "drops") the top element of the stack and has the following definition (slightly rearranged from the Michelson spec)

``code DROP stack _ : S => S type :: _ : 'A -> 'A``

where `_` is a wildcard matching any operations, values, or types

Applying this to our state, our new state is:

``STATE code PUSH string "Hello Tezos!"; NIL operation; PAIR; stack [] type :: []``

The `PUSH` operation adds a value with a certain type onto the top of the stack and has the following definition:

``code PUSH 'a (x :: 'a) stack S => x : S type 'A -> 'a : 'A``

Our concrete instruction is `PUSH string "Hello Tezos!"`, so the transformation is concretized as:

``code PUSH string ("Hello Tezos!" :: string) stack S => "Hello Tezos!" : S type 'A -> string : 'A``

which when applied gives us a new state:

``STATE code NIL operation; PAIR; stack "Hello Tezos!" : [] type :: string : []``

The `NIL` operation adds an empty list of a certain type onto the top of the stack and has the following definition:

``code NIL 'a stack S => {} : S type 'A -> list 'a : 'A``

which when applied gives us a new state:

``STATE code PAIR; stack {} : "Hello Tezos!" : [] type :: list operation : string : []``

The `PAIR` operation removes the top two elements of the stack, makes a pair of them, and pushes the pair onto the stack. It has the following definition:

``code PAIR stack a : b : S => (Pair a b) : S type 'a : 'b : 'A -> pair 'a 'b : 'A``

which when applied gives us a new state:

``STATE code stack (Pair {} "Hello Tezos!") : [] type :: pair (list operation) string : []``

We are now out of operations, and our stack has type `pair (list operation) string : []` which is exactly what we wanted. Since the type matches our expected return type, the contract returns the values in our `(pair 'operations 'storage)`:

``storage  "Hello Tezos!" emitted operations``

This concludes Part I of our Michelson tutorial. You should now know

• the basics of how a stack machine works
• how to install the Tezos client
• how to write and execute a simple michelson contract
• what Michelson types, values and operations are and some simple examples of each one

In Part II, we will write more contracts and go through their execution (although with less rigor), introducing more operations, types and data constructors.

Exercise 1: Modify our `helloTezos.tz` file to output `"Hello World!"` instead of `"Hello Tezos`. Call this file `helloWorld.tz`

Exercise 2: Now modify our `helloTezos.tz` file to take a string argument as input and output `"Hello <input>".` Call this file `helloInput.tz` You will need to know two additional operations to do this:

``code CAR # select left-hand of pair stack (Pair a _) : S => a : Stype pair 'a 'b : 'A -> 'a : 'A``
``code CONCAT # string concatenate stack a : b => a ^ b : S type string : string : 'A -> string: 'A  where a ^ b concatenates the end of a to the beginning of b``

Exercise 3: Do the same thing as exercise 2, except now the contract takes a unit as its input parameter, and outputs `"Hello "` concatenated to its initial storage. So running`\$./alphanet.sh client run script container:hellotezos.tz on storage '"bar"' and input 'Unit'`

should output “Hello bar”. Call this file `helloStorage.tz`

You will need to know one additional operation:

``code CDR # select right-hand of pair stack (Pair _ b) : S => b : S type pair 'a 'b : 'A -> 'b : 'A``

Exercise 4: Write a contract that concatenates an input string and a storage string and ouputs `"Hello <input><storage>"`. call this file`helloInputAndStorage.tz`

You will need to know:

``code DUP # Duplicate the top of the stackstack x : S => x : x : Stype :: 'a : 'A -> 'a : 'a : 'A``
``code DIP ops # Runs code protecting the top of the stackstack x : S => x : S'  where ops / S => S' type :: 'b : 'A -> 'b : 'C  iff ops :: [ 'A -> 'C ]``

You could also use `SWAP` instead of `DIP`

``SWAP # Exchange the top two elements of the stackstack x : y : S => y : x : S type :: 'a : 'b : 'A -> 'b : 'a : 'A``