Because Reading White Papers is Hard #1: Scilla vs Move
In this first episode of Because Reading White Papers is Hard, we cover the design differences between Move and Scilla. If you’re interested in getting Zilliqa’s take on all things crypto, make sure to follow us as we release new episodes.
Cryptocurrencies are now mainstream, thank you Facebook. The crypto world has woken up to the news of Facebook introducing its own blockchain and digital currency project named Libra. We will leave to others the task of debating Libra’s merit as a cryptocurrency. Instead in this article we will focus on reviewing Move, the scripting language for the Libra blockchain. What is Move? How does it compare to Scilla? What is our general takeaway here at Zilliqa? Because we know reading white papers is hard (even though you should), we have the answers for you.
Anton Trunov, our verification expert at Zilliqa, has written an in-depth article illustrating the differences and design choices between Scilla and Move. While we highly recommend Anton’s post, we also want to provide a less technical version of it, one that highlights the salient points of his article. Anton walks us through a use case where Alice has earmarked funds for Bob, showing both Scilla and Move’s implementations, how they differ from each other, revealing the thinking behind each language.
Earmark Use Case
Consider this situation: Bob is going to create an account at address a at some point in the future. Alice wants to “earmark” some funds for Bob so that he can pull them into his account once it is created. But she also wants to be able to reclaim the funds for herself if Bob never creates the account.
We can think of the earmark situation as an escrow, where Alice designates and programmatically locks funds for Bob should he create an account (Bob, a diligent token holder, wants to first read Move’s technical white paper. Of course). Using this scenario, we can highlight two varying approaches to thinking about smart language designs: linearity and global states.
Linearity
The most salient aspect of Move is its use of a linear type system to ensure that objects are used exactly once, and to allow the system to safely deallocate an object after its use. In other words, Move allocates value by creating what it calls resources, which unlike values in typical programming languages, cannot be copied nor can they simply vanish. Linearity enforces accountability.
On the other hand, Scilla uses a type system based on System F, which is not linear. Rather, our approach is to provide tools for formal verification of Scilla contracts, which provides more flexibility in terms of which properties can be established, including the use of SMT-resolver, to formally prove properties that can be expressed in linear integer arithmetic.
Global State
One of the major differences between Move and Scilla is how the languages think of properties. As Anton puts it, Move’s programming model is that of a global bank, where a smart contract changes and modifies the “the global mapping of addresses (representing the “bank”’s clientele) to assets (resources).” With Scilla however, the programming model is more alike to a local bank, where each contract has its “own local mappings of addresses to users’ assets”, and where money is accounted by two internal variables, namely _balance and _amount.
What this points to is different programming approaches, where Move is user-centric and Scilla is contract-centric. Move’s transaction script can call procedures declared by a module to update the global state of the blockchain. While Move’s modules are a lot like Scilla’s contracts, Scilla type system does not track ownership.
For those familiar with design patterns, this is very much like having a singleton class instance to keep track of all your states. And while the use of global states may seem intuitive, it also comes with drawbacks. Providing global access to properties come at a cost of introducing invisible dependencies and tight coupling. Check out global variables are evil and singletons are anti-pattern to read more about the potential drawbacks.
Anton’s post ends by pointing that each of the models includes “different sets of trade-offs and represent user-centric vs bank-centric points of view.” Both Move and Scilla are smart contract languages designed with safety as the first priority, however they use different programming paradigms to achieve the same objective. If you happen to be one of those token holders who cares about the security their funds, you will want to make Scilla Design Story your next reading.
Here’s how you can follow our progress— we would love to have you join our community of technology, financial services, and crypto enthusiasts!
➤ Follow us on Twitter,
➤ Subscribe to our Blog,
