Editor's Note: This article comes from Editor's Note: This article comes fromAmbi Laboratories SECBIT

(ID: SECBIT), author: Guo Yu, founder of SECBIT Lab, released with authorization.

In the field of blockchain, none of the solutions that apply traditional methods will win, and only innovation will have a future.

——Guo Yu

I believe that everyone, like me, was maxed out by Facebook's circle of friends today.

Libra, an encrypted digital currency project initiated by Facebook, officially debuted today (June 18). Libra simultaneously released a multilingual official website and white paper, positioning itself as a global currency and financial service infrastructure for billions of people. Libra has also released several technical white papers detailing its newly developed programming language Move and consensus protocol LibraBFT. The Libra source code has been open sourced on GitHub, and the test network has also been launched. Currently designed as a permissioned chain (consortium chain), it claims that there is no mature solution for the current non-permissioned chain (public chain) that can support the needs of billions of people, and indicates that the transition to the non-permissioned chain will begin within five years of release Work.

Among Libra's series of releases, the new programming language Move is particularly eye-catching. I read the white paper of Move for the first time, well, maybe this is what the smart contract language should look like in the future.

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

A developer from Berlin, Lefteris Karapetsas, put forward his views on social platforms:

Their design goals seem to overlap somewhat, or are they even intended to replace Ethereum?

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

According to CryptoPuzzleDream, founder of PuzzleToLife.com:

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

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.

James Clark, a standards geek, said:

I'm usually skeptical of anything related to cryptocurrencies, but one part of Libra looks quite interesting: a bytecode programming language called Move, whose semantics are inspired by linear logic.

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

secondary title

Three Useful Uses of the Move Language

• Issue digital currency, Token, and digital assets

• secondary title

Bottom-up static type system

Bottom-up static type system

Well-typed programs never get stuck.

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 adopt static type systems. Their advantage is that many low-level programming errors can be found at compile time instead of being delayed until runtime. bug.

This is a slang term in the programming language (PL) world: a type-correct code will never run away. Meaning, if a piece of contract code is type-checked, the reliability will be quite high.

secondary title

First-class Resources Philosophy

First-class Resources Philosophy

The word First-class Resources is quite academic. In Chinese translation, resources are first-class citizens. What does this mean?

The so-called first-class citizens of the programming language are the programming objects that the programming language first considers when programming.

So resources, what are Resources? It's also a very academic name. Resources is a concept corresponding to Value. Value can be copied at will, while Resources can only be consumed, not copied. Resources are like Coke, if you drink a bottle, you will lose one bottle, and Value is like an English word written in a notebook, you can read it every morning, and it will not disappear after reading it, if you remember it, then Just made a copy in my head. Not only can you read it, but I can also read it, you can recite it, and I can recite it too.

Traditional programming languages, including the Ethereum smart contract language, adopt the Value method for bookkeeping of digital assets, which leads to a problem: it is possible to make mistakes in bookkeeping. In fact, there are quite a lot of smart contracts with misrecorded accounts. For example, when Zhang San transfers money to Li Si, Li Si’s account has an extra 10 yuan, but Zhang San’s account balance has not changed. Various bookkeeping loopholes in the past two years have even caused everyone to lose confidence in the future of smart contracts.

• The Move contract adopts a type that absorbs the traditional theory of "linear logic", called a resource type. Digital assets can be defined by "resource type". In this way, digital assets, like resources, satisfy some characteristics in linear logic:

• Digital assets cannot be copied

• Digital assets cannot disappear in thin air

The real meaning of First-class Resources is that digital assets are first-class citizens. This sentence can be extended to the fact that Move is a smart contract language for operating digital assets. From a technical point of view, digital assets can be used as contract variables, digital assets can be stored, assigned values, used as parameters of functions/procedures, or as return values ​​of functions/procedures. And Move's static type system enables smart contract code to check out most resource usage errors through the compiler during compilation, that is, before deployment. Guaranteed smart contracts are no longer as fragile as they used to be.

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. Resources as first-class citizens are a very general concept, Programmers can use it not only to implement secure digital assets, but also to write correct business logic and implement correct access control policies.

secondary title

Contract Security Design

The Move contract was designed with full consideration of security. First of all, Move does not support dynamic assignment (Dynamic Dispatch). Okay, let me explain what Dynamic Dispatch is. In layman's terms, this is a very flexible language mechanism. Many functions, procedures, or subroutines can be written in the program. Then a main program can call these functions/procedures/subroutines to complete different functions respectively. If the program is running, we can know which function it calls, or call many functions in a certain order, then these function calls are "static", if before running, we don't know the function call of a certain step Which function is called, until the program is running, we can only know through observation, then this function call is called "dynamic". "Dynamic" is obviously more flexible than "static".

But being flexible also means being more prone to problems. 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 features are not conducive to program reasoning, even less conducive to formal verification (Formal verification), and are more likely to cause security problems. There are many "dynamic features" in the design of Ethereum smart contracts, such as supporting function pointers as parameters, contracts as parameters, delegatecall, etc. In the Move language, it does not support any form of "dynamic assignment" or "dynamic features". All contract execution paths can be determined at compile time, and then can be fully analyzed and verified.

Before the Move contract is run, it will be verified by a bytecode verifier (Bytecode verifier), which can check out various types of errors. At the same time, when the bytecode is interpreted and executed, it still carries the type, and it is checked while running.

Compared with the Ethereum EVM platform, the Move module system does not support circular recursive dependencies, which perfectly solves the contract re-entrancy vulnerability (Re-entrancy).

secondary title

Powerful module system

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 Move module system is designed in a functional programming language (OCaml, Coq, SML) style, according to the white paper:

Move's module system provides a very good foundation for the formal verification of smart contracts, and "invariants" 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 module system can make the formal verification work modular and lower in cost. Writing program analyzers and symbolic executors on the Move module system will be much simpler, because after abstraction, the contract logic can be made very simple and easy to reason.

text

Future-proof Move Smart Contract

Although Move seems a little rough and immature, this direction is still exciting. From the Move language level, we can see Facebook's ambition to be a huge digital asset platform. This role should have belonged to Ethereum.

• Why I fell in love with Move a little bit, after thinking about it, there are probably three reasons:

• It has absorbed the research achievements in the field of PL (programming language), and also absorbed the experience and lessons of the EVM smart contract language

• The design attaches great importance to "smart contract security and correctness"