---
title: Scilla Design Principles
---

[Smart contracts]{.title-ref} provide a mechanism to express computations on a
blockchain, i.e., a decentralized Byzantine-fault tolerant distributed ledger.
With the advent of smart contracts, it has become possible to build what is
referred to as [decentralized applications]{.title-ref} or Dapps for short.
These applications have their program and business logic coded in the form of a
smart contract that can be run on a decentralized blockchain network.

Running applications on a decentralized network eliminates the need of a trusted
centralized party or a server typical of other applications. These features of
smart contracts have become so popular today that they now drive real-world
economies through applications such as crowdfunding, games, decentralized
exchanges, payment processors among many others.

However, experience over the last few years has shown that implemented
operational semantics of smart contract languages admit rather subtle behaviour
that diverge from the [intuitive understanding]{.title-ref} of the language in
the minds of contract developers. This divergence has led to some of the largest
attacks on smart contracts, e.g., the attack on the DAO contract and Parity
wallet among others. The problem becomes even more severe because smart
contracts cannot directly be updated due to the immutable nature of blockchains.
It is hence crucial to ensure that smart contracts that get deployed are safe to
run.

Formal methods such as verification and model checking have proven to be
effective in improving the safety of software systems in other disciplines and
hence it is natural to explore their applicability in improving the readability
and safety of smart contracts. Moreover, with formal methods, it becomes
possible to produce rigorous guarantees about the behavior of a contract.

Applying formal verification tools with existing languages such as Solidity
however is not an easy task because of the extreme expressivity typical of a
Turing-complete language. Indeed, there is a trade-off between making a language
simpler to understand and amenable to formal verification, and making it more
expressive. For instance, Bitcoin\'s scripting language occupies the
[simpler]{.title-ref} end of the spectrum and does not handle stateful-objects.
On the [expressive]{.title-ref} side of the spectrum is a Turing-complete
language such as Solidity.

[Scilla]{.title-ref} is a new (intermediate-level) smart contract language that
has been designed to achieve both [expressivity]{.title-ref} and
[tractability]{.title-ref} at the same time, while enabling formal reasoning
about contract behavior by adopting certain fundamental design principles as
described below:

## Separation Between Computation and Communication

Contracts in Scilla are structured as communicating automata: every in-contract
computation (e.g., changing its balance or computing a value of a function) is
implemented as a standalone, atomic transition, i.e., without involving any
other parties. Whenever such involvement is required (e.g., for transferring
control to another party), a transition would end, with an explicit
communication, by means of sending and receiving messages. The automata-based
structure makes it possible to disentangle the contract-specific effects (i.e.,
transitions) from blockchain-wide interactions (i.e., sending/receiving funds
and messages), thus providing a clean reasoning mechanism about contract
composition and invariants.

## Separation Between Effectful and Pure Computations

Any in-contract computation happening within a transition has to terminate, and
have a predictable effect on the state of the contract and the execution. In
order to achieve this, Scilla draws inspiration from functional programming with
effects in distinguishing between pure expressions (e.g., expressions with
primitive data types and maps), impure local state manipulations (i.e.,
reading/writing into contract fields), and blockchain reflection (e.g., reading
current block number). By carefully designing semantics of interaction between
pure and impure language aspects, Scilla ensures a number of foundational
properties about contract transitions, such as progress and type preservation,
while also making them amenable to interactive and/or automatic verification
with standalone tools.

## Separation Between Invocation and Continuation

Structuring contracts as communicating automata provides a computational model,
which only allows [tail-calls]{.title-ref}, i.e., every call to an external
function (i.e., another contract) has to be done as the absolutely last
instruction.