Move language: Libra's biggest highlight in my eyes

In the field of blockchain, no solution wins the traditional method, only innovation can have a future.

——Guo Yu

I believe that everyone, like me, is being smashed by Facebook today.

Libra, a Facebook-sponsored encrypted digital currency project, officially made its debut today (June 18). Libra has simultaneously released a multi-language official website and white paper, targeting the global monetary and financial services infrastructure for billions of people. Libra also released several technical white papers detailing its newly developed programming language Move and the consensus protocol LibraBFT. The Libra source is open sourced on GitHub and the test network is online. Currently designed as a licensing chain (chain of alliances), it claims that the current non-licensed chain (public chain) does not have a mature solution that can support the use of billions of people, and that it will begin to transition to the non-licensed chain within five years of release. jobs.

• A brief analysis of the currency attributes of Facebook's digital currency Libra
• Facebook currency, these 6 points you need to know
• Is Libra just a stable currency project?

In a series of Libra releases, the new programming language Move is particularly eye-catching. The first time I saw Move's white paper, um, this may be what the future smart contract language should look like .

A developer from Berlin, Lefteris Karapetsas, put forward his own views on the social platform:

Their design goals seem to overlap, or even aim to replace Ethereum?

Their design goals seem to overlap, or even to replace Ethereum?

CryptoPuzzleDream, founder of PuzzleToLife.com, believes that:

I think "move" programming language released by $FB could be more interesting than libra.

I think the "move" language released by FB is more interesting than libra.

James Clark is a standard geek who says:

I'm usually pretty skeptical of anything related to cryptocurrency, but here's one piece of Libra that looks potentially interesting: a bytecode programming language called Move with semantics inspired by linear logic.

I usually doubt anything about cryptocurrencies, but some of Libra seems quite interesting: a bytecode programming language called Move, whose semantics are inspired by linear logic.

And my flash in my head is such a sentence:

Move is a smart contract platform language for "digital assets."

The three major uses of the Move language

1. Issue digital currency, Token, and digital assets
2. Flexible handling of blockchain transactions
3. Validator management

Bottom-up static type system

Move uses a static type system, which is essentially a logical constraint. It is much stricter than Ethereum's smart contract language. Modern programming languages ​​such as Rust, Golang, Typescript, Haskell, Scala, and OCaml all use static type systems. Their advantage is that many low-level programming errors can be found at compile time, rather than being dragged to the runtime. Bug.

Well-typed programs never get stuck.

This is an slang in the field of programming languages ​​(PL): a type of error-free code never runs. This means that if a contract code is type checked, the reliability will be quite high.

Move is also not designed as a 100% static type check language, which will reduce the usability. Move mentions trying to make type checking as much as possible at compile time, rather than waiting until it is deployed on the chain. Of course, some types of checks have to be put into the run, but still can be type safe.

Move has a very good design idea, from the beginning of the virtual machine is statically typed, and then up is an intermediate language layer, IR (Intermediate Representation), is also typed. In the future, the upper layer of Move will provide more high-level languages ​​for various financial applications. These languages ​​are naturally static types, ensuring that smart contracts no longer have very low-level errors.

First-class Resources concept

The term " First-class Resources " is quite academic. Chinese translation means that resources are first-class citizens . What does this mean?

The first-class citizen of the so-called programming language is the programming object that the programming language first considers when programming.

So resources, what is Resources ? This is also a very academic name. Resources is a concept that corresponds to Value. Value   Is free to copy, and Resources   Can only be consumed and cannot be copied. Resources is like a cola. You drink one bottle and you have one bottle. Value is like an English word written on the book. You can read it every morning. If you finish it, it won't disappear. If you remember, then Just copied a copy in my head. Not only can you read, but I can also read, you can recite, and I can recite it.

Traditional programming languages, including the Ethereum smart contract language, use the Value method for accounting of digital assets, which leads to a problem: billing is possible to be mistaken. In fact, the smart contract for miscounting is quite a lot. For example, Zhang San transferred to Li Si, and Li Si’s account has 10 yuan more, but Zhang’s account balance has not changed. The various accounting loopholes in the past two years have even caused everyone to lose confidence in the future of smart contracts.

The Move contract uses a type that absorbs the traditional theory of "linear logic," called a resource type. Digital assets can be defined by "resource types", so that digital assets, like resources, satisfy some of the characteristics of linear logic:

1. Digital assets cannot be copied
2. Digital assets cannot disappear out of thin air

The true meaning of First-class Resources is that digital assets are first-class citizens . This sentence can be derived. Move is a smart contract language for operating digital assets. From a technical point of view, a digital asset can be used as a contract variable, a digital asset can be stored, can be assigned, can be used as a function/procedure parameter, or as a function/process return value. Move's static type system allows smart contract code to check for most resource usage errors through the compiler at compile time, which is before deployment. Keep smart contracts no longer as fragile as they used to be.

Extract a sentence from the abstract of the white paper:

First-class resources are a very general concept that programmers can use not only to implement safe digital assets but also to write correct business logic for wrapping assets and enforcing access control policies. As a first-class citizen, resources are a very common concept. Not only can programmers use it to implement secure digital assets, but they can also write the right business logic to achieve the right access control strategy.

Contract security design

The Move contract is designed with full consideration for security. First, Move does not support Dynamic Dispatch at all. Ok, I am here to explain what is Dynamic Dispatch. In layman's terms, this is a very flexible language mechanism . Inside the program are a lot of functions, or procedures, or subroutines. Then a main program can call these functions/procedures/subroutines to perform different functions. If the program is running before we can know which function it calls, or call a lot of functions in some order, then these function calls are "static". If we run it, we don't know the function call of a step. Which function is called, until the program is running, through observation, we can know, then this function call is called "dynamic". "Dynamic" is obviously more flexible than "static".

But flexibility also means that problems are more likely to occur. Many modern programming languages ​​support dynamic assignment more or less, that is, direct support from the language level, such as "dynamic binding" caused by "inheritance" in object-oriented languages. Dynamic characteristics are not conducive to program reasoning, more detrimental to Formal verification, and more likely to cause security problems. There are many "dynamic features" in the Ethereum smart contract design, such as support function pointers for parameters, contract parameters, delegatecalls, and so on. In the Move language, there is no support for any form of "dynamic assignment" or "dynamic characteristics". All contract execution paths can be determined at compile time, and then can be fully analyzed and verified.

The Move contract is checked by a Bytecode verifier before it can run. This validator can check for various types of errors. At the same time, when the bytecode is interpreted and executed, it still carries the type, while running, checking.

The Move language imposes very strict restrictions on contract modifiable variables and steals some design ideas from the Rust language. It is guaranteed that the modifiable variable can only be modified by a pointer at any time, so that it will not cause confusion. In Ethereum Solidity, you can define a lot of pointers to the same variable. If the code logic is not considered clearly, it will be very easy to go wrong.

Compared with the Ethereum EVM platform, the Move module system does not support cyclic recursive dependencies, which perfectly solves the contract re-entrancy.

Powerful modular system

The Move module system uses a functional programming language (OCaml, Coq, SML) style design, according to the white paper:

Move modules are similar to smart contracts in other blockchain languages. …, However, modules enforce strong data abstraction — a type is transparent inside its declaring module and opaque outside of it.

The modular system can package the concept of digital assets well, and the operation of digital assets, such as through the module's public interface, and flexible permissions control on this interface. When writing the Ethereum smart contract, the ERC20 Token on Ethereum exists as a contract. In the Move language, a Token can be imagined as a box, which is passed as a resource, but does not expose the box. Internal details. At the same time, the abstraction of the module system is also based entirely on its static type system, and type safety can be checked by the smart contract virtual machine.

Move's modular system provides a very good foundation for formal verification of smart contracts, and "invariant" can be defined inside the module. The so-called invariant refers to a strict constraint on the internal state of digital assets, which can provide very valuable information for the automation of formal verification. Moreover, the "opaque abstraction" of the modular system can make formal verification work modular and less expensive. Writing a program parser on a Move module system, symbolic executors are also much simpler, because abstraction can make contract logic very simple and easy to reason.

Future-oriented Move Smart Contract

Move Although it looks a bit rough and immature, this direction is still exciting. From the Move language level, you can see Facebook's ambitions and want to be a huge digital asset platform. This role should have belonged to Ethereum.

Why do I like the Move a bit, think about it, for the following three reasons:

1. Drawing on the research results in the PL (programming language) field, and also absorbing the lessons of the EVM smart contract language
2. From the design, we attach great importance to "smart contract safety and correctness"
3. There is no stickiness (not using WASM, LLVM, or directly modified on EVM), but active innovation, is a smart contract language that is designed to be truly suitable for financial applications.

Author: Yu Guo

Source: Ambi Labs SECBIT

We will continue to update Blocking; if you have any questions or suggestions, please contact us!