LOVE: a New Smart Contract Language for the Dune Network

David Declerck
Jan 22, 2020 · 5 min read

By De Oliveira Steven & David Declerck

Context

In a few words, Love is designed to be expressive for fast development, efficient in execution time and cheap in storage, and readable for auditability of smart contracts. Yet, it has a clear and formal semantics and a strong type system to detect bugs. It allows contracts to use other contracts as libraries, and to call viewers on other contracts. Contracts developed in Love can also be formally verified.

Why Love ?

At one end of the scale, we have very low-level languages such as Michelson: it has a limited expressiveness due to its reduced set of instructions and does not allow code sharing, rendering the writing of even simple contracts a time consuming and error-prone task. Its lack of readability makes smart contract auditing difficult. However, it has been designed with formal verification in mind, which helps writing formal analysis tools for smart contracts — although we may argue that formal verification of low-level code is not an easy task.

At the other end of the scale, we have very high-level languages like Solidity: it is an expressive and feature-rich language, allowing to easily write a broad range of smart contracts, but does not offer strong safety guarantees. Moreover, the code running on the blockchain is not the Solidity code itself, but the result of its compilation to EVM bytecode: once deployed, it is hard to tell what a contract really does.

Love has been designed to be in between: sufficiently high-level and expressive, yet also low-level in the sense that it is directly executed on the blockchain. This allows writing and reviewing/auditing smart contracts easily, and opens the door to a wide range of formal verification methods.

A comparison of smart contracts in Michelson, Solidity and Love

Love version

#lovetype storage = {
total : dun;
calls : nat;
}
val%init storage (_ : unit) = {
total = 0.0dn;
calls = 0p;
}
val%entry main (s : storage) (amount : dun) (_ : unit) =
let total = s.total +$ amount in
let calls = s.calls ++ 1p in
[][:operation], { total; calls }

This code is stored and executed under this form on the blockchain. Love contracts are both readable and efficient.

Michelson version

parameter unit;
storage (pair mutez nat);
code { CDR ;
PUSH nat 1 ;
DUUP ;
CDR ;
ADD ;
AMOUNT ;
DUUUP ;
DIIIP { DROP } ;
CAR ;
ADD ;
PAIR ;
NIL operation ;
PAIR };

A notable aspect of this language is the ubiquitous use of DIP, DUP and SWAP to manipulate the stack. Despite targeting formal verification, its lack of readability makes contract auditing a nightmare.

Solidity (source) version

pragma solidity >=0.4.0;contract Count {uint total = 0;
uint calls = 0;
function main() public payable {
total += msg.value;
calls += 1;
}
}

Despite its popularity, Solidity trades simplicity and expressiveness for safety and reliability, which is illustrated by tens of stories of huge losses due to bugs.

EVM bytecode generated for the Solidity version (excerpt)

JUMPDEST
CALLVALUE
PUSH1 0x00
DUP1
DUP3
DUP3
SLOAD
ADD
SWAP3
POP
POP
DUP2
SWAP1
SSTORE
POP
PUSH1 0x01
DUP1
PUSH1 0x00
DUP3
DUP3
SLOAD
ADD
SWAP3
POP
POP
DUP2
SWAP1
SSTORE
POP
*JUMP

EVM is even harder to read than Michelson and provides no formal basis guarantees.

Comparison of Space Usage

Key differences between LOVE and other languages

Going Further

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

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 ( http://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 ( http://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.