The Love Smart Contract Language: Introduction & Key Features — Part I

David Declerck
Feb 1, 2020 · 7 min read

By De Oliveira Steven & David Declerck

What Is Love?

Love is a new native smart contract language for the Dune Network, meant to coexist alongside with Michelson. Also designed with formal verification in mind, Love offers new exclusive features to improve smart contracts design and implementation, among which:

  • direct read-only access to another contract’s storage
  • library contracts that can be either statically or dynamically referenced
  • easy-to-read target language for higher-level languages
  • high-level enough so that contracts can also be directly written in Love.

In this first article, we will introduce the basics of the language. The next article, Part 2, will introduce the module system, used to easily compose smart contracts.

Why Love?

The former smart contract language on the Dune Network, Michelson — inherited from Tezos — has been designed with its implementation using GADTs in mind. GADTs are a powerful feature of the OCaml type-system, but they come with many drawbacks: they make the language limited, constrained and hard to change. As a result, anyone who tried to write a (non-trivial) smart contract in Michelson knows how tedious it can be: it has a very restricted set of instructions, is rather hard to read for the uninitiated (and not straightforward for the initiated), making contract auditing an almost impossible task, and its stack is tricky to deal with. In particular, accessing variables requires to constantly remember their position in the stack and the current stack height, which is error-prone. This also makes it harder to use Michelson as a target language for compilation.

With this in mind, and notwithstanding the qualities of the Michelson language, we wanted to offer a more general-purpose alternative language, hence Love, also amenable for formal verification.

Basic Contract Structure

Love is a functional language, and borrows its syntax both from Liquidity and OCaml. As Love is a target language, developers are not supposed to write directly in Love. In this article, we will still write some contracts in Love, to better understand how it works.

Before entering the details of the language, let’s start with a simple smart contract that counts how many times it was called and how many DUNs it received:

All Love smart contracts share the same basic structure. The very first line must begin with a #love directive, to distinguish them from the Michelson smart contracts (which should now start with a #mic directive, although if missing, the language will default to Michelson).

Then follows one or more type declarations, one of them being the mandatory storage type declaration, which specifies the layout of the contract data. As in Liquidity and OCaml, these can be either record types, sum types, tuples, or just aliases to other types. In the above example, the storage type is a record containing two fields, total of type dun (the type of amounts) and calls of type nat (natural numbers). Many different types exist, such as bool, int, string, bytes, keyhash, address… You may refer to the Love documentation for a complete list of types.

After this, a storage initializer should be specified. It is a unique function named storage, introduced with val%init and having a single argument, used to produce the initial storage of the contract when it is originated. If a storage initializer is not specified, then the programmer will have to manually build an initial storage in order to originate the contract. In our example, the storage initializer does not use its argument, so it is given a type unit and no name. It sets the field total to 0 DUN and the field calls to 0. Notice how these constants are written: an amount in DUN ends with dn, and a natural number ends with p (whereas an integer would have no suffix). Check the documentation for how to write constants in Love.

Finally, a contract defines one or more entrypoints, which are functions introduced with the val%entry keyword and which take three arguments: the contract storage, the transaction amount, and a parameter. The type of the two first argument is fixed, thus it is not mandatory to specify them. Also, entrypoints return a pair of values: a (possibly empty) list of operations (transactions or originations), and the new value of the storage. The returned operations are performed after the contract has finished its execution. In our example, the entrypoint main adds the amount of duns received to the total amount of DUN memorized in the storage s, increments the number of calls by one, builds a new storage with these values, and returns a pair composed of an empty list of operations and this new storage.

Two important aspects of the Love language are displayed in this simple contract:

  • First, unlike in Liquidity (and many other languages), we used different addition operators: we used +$ to add duns and ++ to add naturals (and we would just have used + on integers). Indeed, there is no operator overloading in Love, so each operator works on specific types. All these operators and their naming scheme are detailed in the documentation.
  • Secondly, to build the empty list of operations, we wrote [][:operation]: indeed, the empty list constructor [] is polymorphic, i.e. it allows to construct a list of anything, so the type of elements contained in the list must be specified. This mechanism is ubiquitous in Love, and should be understood properly to use Love at its best. It is further described in the next section.

Functions, Recursion and Polymorphic Functions


Similarly to how entrypoints are defined, one may also define functions. A function is introduced by the val keyword, followed by its name, the list and type of its arguments, and its return type. For instance:

This defines a function add_and_sub that takes two integers as argument and returns a pair of integers. This function will be visible from the outside, so other smart contracts may call it. This can be prevented by declaring the function with val%private instead of val.

User-defined functions can then be used as any other Love built-in function. For instance, to use the add_and_sub function defined above, we may write:

It is also possible to declare functions locally, in another function or entrypoint. In this case, the function is introduced with a let ... in construct, and its return type does not need to be specified:

Here, the function double is local to the entrypoint main.

Recursive Functions

Love also supports recursive functions, useful for simulating loops and iterating over collections. Such functions are introduced with val rec or let rec ... in , and their return type must always be specified (even when defined locally). For instance:

This defines a (local) recursive function mul_pow_2, that (inefficiently) computes x * 2 ^ t, and uses it on the contract’s storage.


Many Love primitives are designed to work with values of different types: they are said to be polymorphic. This is the case for primitives on collections (for instance lists, sets and maps, that may contain either integers, strings, records…), as well as comparison operators.

To use these primitives and operators, one has to explicitly specify the type of its argument, by performing what we call a type application. This is achieved by passing one or more arguments of the form [:type] to the primitive or operator. For instance, in the previous example, we applied the type nat to the = operator by writing = [:nat]. Note that in this particular case, the type could be omitted and inferred automatically, since one of the operands is a constant.

Love also allows the programmer to define his own polymorphic functions. This is achieved by adding type variables as arguments to the function, and then using these to specify the types of actual arguments. Type variables are introduced using a ' symbol. Here is an example of a user-defined polymorphic function:

Calling such a function simply requires passing the types as arguments, as we would do with polymorphic primitives:

Note that type arguments do not specifically have to be placed first in a function declaration. For instance, one could write:

This function would then be called as follows:

The interested reader may refer to literature about System-F for the theoretical background.

Closing Words

This concludes Part 1 of our technical introduction to Love. In the next part, we’ll see how to better structure a smart contract through the use of modules, and discuss how to implement contract interactions, i.e. how a contract can create or call another contract and read its storage through views. Meanwhile, don’t hesitate to follow the Love tutorial and to read the documentation.

EDITED: check our next article on Love: The Love Smart Contract Language: Introduction & Key Features — Part II

These are some of the resources you might find interesting in building your own smart contracts:

And other resources on the Dune Network:

Dune Network

Blog, updates, and technical articles on the Dune Network

Dune Network

Dune Network ( ) is a 3rd-generation blockchain platform, with a focus on security and accessibility. Its main features are delegated Proof-of-Stake, multiple native smart contract languages, formal verification and easy private chains deployments.

David Declerck

Written by

Dune Network

Dune Network ( ) is a 3rd-generation blockchain platform, with a focus on security and accessibility. Its main features are delegated Proof-of-Stake, multiple native smart contract languages, formal verification and easy private chains deployments.

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store