# Introduction to Smart Contracts in Tezos

## What is Michelson?

Michelson is the domain-specific language used to write smart contracts on the Tezos blockchain. Michelson is a stack-based language, and it doesn't have any variables. Stack-oriented languages operate on one or more stacks, each of which may serve a different purpose.

See here for Michelson documentation and here for the camlCase Michelson tutorial series.

## What is Liquidity?

Liquidity is a high-level language used to program Smart Contracts for Tezos. It is a fully typed functional language. It uses the syntax of OCaml, and it strictly complies with Michelson security restrictions. Liquidity already covers 100% of the Michelson features, and contracts generated with Liquidity can be submitted on the main network. Developers are currently working on a formal-method framework that will be used to prove the correctness of smart-contracts written in Liquidity.

## What is the difference between Liquidity and Michelson?

Liquidity is compiled strictly back to Michelson. As a language, Liquidity is easier for many developers to approach as it has an easier syntax, local variables, and high-level types rather than stack manipulations. A formal verification framework for Liquidity is under development.

## What is OCaml, the language of the Tezos protocol?

The Tezos protocol is written in OCaml, a general purpose industrial-strength programming language with an emphasis on expressiveness and safety. It is the technology of choice in companies where speed is crucial and a single mistake can cost millions. It has a large standard library, which makes it useful for many of the same applications as Python or Perl, and it has robust modular and object-oriented programming constructs that make it applicable for large-scale software engineering. Many top companies use OCaml, including Facebook, Bloomberg, Docker, and Jane Street.

## What is functional programming? How is it different from other paradigms?

Functional programming is a programming paradigm — a style of building the structure and elements of computer programs — that treats computation as the evaluation of mathematical functions and avoids changing-state and mutable data.

It is a declarative programming paradigm, which means programming is done with expressions or declarations instead of statements. In functional code, the output value of a function depends only on the arguments that are passed to the function, so that calling a function f twice with the same value for an argument x produces the same result f(x) each time. This is in contrast to procedures that depend on a local or global state, which may produce different results at different times when called with the same arguments but a different program state. Eliminating side effects, i.e. changes in state that do not depend on the function inputs, can make it much easier to understand and predict the behavior of a program, which is one of the key motivations for the development of functional programming.

Here is a diagram that shows the high-level differences between the EVM (Ethereum Virtual Machine), WASM (Web Assembly) and Michelson:

# Introduction

Michelson is the low-level, stack-based programming language used to write smart contracts on the Tezos blockchain. Michelson was designed to facilitate formal verification, allowing users to prove the properties of their contracts.

It 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: Wikipedia.

# 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 ꜩ, 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.

# "Why Michelson?" (by Milo Davis)

At first sight, Michelson is a strange language. It doesn’t include features like polymorphism, closures, or named functions. Compared to a language like Haskell or OCaml, it seems underpowered. Its stack is not always easy to deal with, and there is no standard library. However, these restrictions are largely motivated by the language’s design goals.

There are two major motivations for Michelson:

2. To be introspectable

Tezos takes a slightly different view from Ethereum regarding the role of smart contracts. We think of our platform more as a way to implement certain pieces of business logic than as a generic “world computer." In Ethereum, most contracts implement things like multisig wallets, vesting and distribution rules, etc. Michelson is targeted to these types of applications.

Michelson is designed as a readable compilation target, though it can be handwritten. The goal is that even the output of a compiler can be understood. We intend the language to be simple enough that developers can build their own analysis tools and compilers should they prefer to do so. This is a departure from the EVM’s bytecode, which more closely resembles assembly. With a lower-level bytecode, you usually need confidence in both your program and the compiler toolchain. With Michelson you can more easily check over and verify properties of the program that is actually executed.

Using a higher-level bytecode also simplifies the process of proving properties about the compiled output. Programs written in Michelson can be reasonably analyzed by SMT solvers and formalized in Coq without the need for more complicated techniques like separation logic. Similarly, the restrictions imposed by the forced indentation and capitalization ensure that the source cannot be obfuscated with indentation and alignment tricks.

Our current implementation of Michelson is based around an OCaml GADT, which we have used to verify the type-soundness of the language. Additionally, the implementation of a stack based language maps directly to the semantics. The same is not true for any efficient implementation of the lambda-calculus. There have also been two formally verified implementations of Michelson, one in Coq and one in F*. One day, we hope to replace our current implementation with a verified one.

Finally, one of the main advantages of Tezos is that the system is amendable. We want to start with a small core language in which we are confident and add features as good use cases are created for them. We don't want to throw everything into the language in at the onset and then break backwards compatibility.

So, why Michelson? To provide a straightforward platform for business logic, to provide a readable bytecode, and to be introspectable. When I was working with Olin Shivers, he was very fond of saying that one should always use a "tool small enough for the job". Michelson has been carefully designed to be that tool.

# Liquidity

Liquidity is a high-level language to program Smart Contracts for Tezos. It is a fully typed functional language, it uses the syntax of OCaml, and it strictly complies with Michelson security restrictions.

Developers are currently working on a formal-method framework that will be used to prove the correctness of smart-contracts written in Liquidity.

The Liquidity language provides the following features:

• Full coverage of the Michelson language: Anything that can be written in Michelson can be written in Liquidity,
• Local variables instead of stack manipulations: values can be stored in local variables.
• High-level types: types like sum-types and record-types can be defined and used in Liquidity programs.

Liquidity already covers 100% of the Michelson features, and contracts generated with Liquidity can be submitted on the current mainnet and zeronet.