Move, is it that good?

Recently, Aptos and Sui have been in the spotlight of the crypto community; among all the news, their heritage from Diem —- Move the programming language, which is now adopted by both Aptos and Sui blockchain, is the most crucial innovation for this newly created ecosystem.

Let's dive in to take a look at the most crucial things Move has to provide.

First-class resources: Move being the smart contract programming language is born to deal with digital assets. This means that it needs to possess an ability to encode the various assets and corresponding business logic that make up the financial infrastructure.

In Move, an asset is not a hash, not a string, but a specially defined code, represented by /resource/ or stored in it. Move abstracts four attributes of resources, which can be copied (copy), and is indexable (key), discardable (drop), and storable (store). Users can quickly define any resource through combinations of these four attributes. This is undoubtedly one of the many innovative features of Move. The resource-first concept is an excellent help for programmers to write safe and efficient code in a way that enhances the possibility of composability as an asset is a type by itself, which opens up a lot of possibilities in general programming. Meanwhile, in Solidity, assets are not explicitly defined, they are just treated like any other variables. 

Apart from the above-mentioned benefits, this feature makes Move more resistant to some of the known blockchain attacks such as Reentrancy. The Reentrancy attack is one of the most destructive attacks in Solidity smart contracts. A reentrancy attack occurs when a function makes an external call to another untrusted contract. Then the untrusted contract makes a recursive call back to the original function in an attempt to drain funds.

An Aptos’ medium article precisely stated the feature as “a resource can never be copied or implicitly discarded, only moved between program storage locations”, which makes it possible for Move to effectively avoid the aforementioned attack. What’s more, compared to EVM, the modular system supports cyclic recursion dependency, which makes the occurrence of the Reentrancy bug impossible. 

Next up, let’s take a close look at Move’s other important feature - Static typing.

Let’s stop here for a bit and quickly revise how we distinguish static calls from dynamic calls. In layman's terms, when a program calls another program, if the called target can only be determined during runtime, it is recognized as a dynamic call; on the contrary, if the called target can be determined before executing and cannot be changed, the call is recognized as a static call.

Move’s structure sets each function call to be static, and the developer knows exactly when to call a function. This static type system presupposes the exposure of the problem to the compilation phase, not the runtime phase, reducing the chance of a crash during runtime.

A very popular technical jargon among coders is that “Well-typed programs never get stuck”. What it is trying to say is that “If a code is type checked, then the reliability is quite high”.    Indeed, but is it worth it to design it this way to an almost extreme extent for the sake of “security”? What is the trade-off between security and creativity here?

One thing we can be sure of is that Move is not designed to be 100% static typing, as it will greatly lower its usability. In fact, we can find that Move has found its balance point between Ripple and Ethereum’s characteristics.

If we examine Ripple closely, we can see it is a decentralized financial system itself. There is no need to build any Defi projects on it. It itself is an order book, and at the same time, it restricts the types in such an extreme sense and technically does not support innovation.

With the above being said, we can see that one of Move’s potential issues is that it could limit the creativity and innovation of its adopters. For example, I might not be able to separate the ownership rights and usage rights of an NFT with Move, as there could be a lot of data I can’t access. 

Lastly, let's discuss its security feature.

Let’s ask ourselves a question, what would happen if the smart contract code we wrote contains bugs/loopholes? What are the consequences? I believe all of us have the unanimous consensus that any bugs would be intolerable, despite their severity.

You might wonder why do we see so many attacks on loopholes arise from Dapps within the Ethereum ecosystem? The answer is that since the development efficiency and scenario iterations are very fast in the Internet era, the tolerance for bugs has increased accordingly (the mentality being, as long as it is not a significant problem, we can always fix it after we ship the MVP). Besides, most blockchain developers are from the somewhat “traditional“ Web2 industry Unless the Web3 common sense “code is money” really resides with the developers, their experience and habits from working in Web2 can potentially expose projects to more security risks. 

Another way to view this issue is that the security risks of Solidity itself are mostly due to the introduction of “Gas” from Ethereum, which led to the rise of a new category of loopholes we have never encountered before. For example, the smart contract itself has no loopholes, but the attacker can adjust the gas fee to attack and halt the smart contract at some intermediate step. These problems are completely novel among traditional developers. With almost all blockchains having the gas feature, they are all vulnerable to this issue. 

With the innovation of Move Prover, Move has the ambition to fix most of the security issues once and for all, but does it have the ability to do so?

**“The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language.”**

The developers behind Move believe that traditional software is large and complex, which makes it difficult to verify the language features used even in the simplest tasks. However, Move Prover has the potential to be adopted by most Move developers.

Before we dive deeper into it, we need to understand what Formal Verification is.

According to Wikipedia, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

Basically, we list out a bunch of rules and regulations in the programming language to see if your code has violated them. This is formal verification.

Formal verification was first integrated into the circuit (CPU). Using formal verification to verify low-level programming languages such as C or C++ (low-level language) is relatively simple, as the information provided by such languages is usually a lot less abstract. Codes that can be done in 3 lines if writing with more advanced programming languages needs to be done in 30 or even 300 lines in low-level programming languages. The reason being the more abstract the code is, the more loopholes it presents. You can think of it as the more abstract the content, the more interpretation there will be. Take Solidity for example, there is no such thing as one rule fits all when it comes to the formal verification of Solidity smart contracts. The only things we can rely on when evaluating whether a program is appropriate are past experience (adding issues discovered in the past to unit test cases), the developer’s experience, and testing. In this regard, maybe it is safe to draw the conclusion that the more advanced the programming language is, the more complicated the formal verification will be. 

In that case, to what extent can the Move Prover achieve in terms of integrating Formal Verification? My guess is that it may be able to conduct some sort of very simple formal verification, but for the more complicated components, professional smart contract auditors’ assistance will be a must.

I believe that we should always consider both sides no matter how well it is presented, adhering to the spirit of exploration and questioning, which is the intention of this report too. Although Solidity has been through numerous challenges and stands till today as a smart contract programming language, it is considered a very young programming language in a broader comparison with the other more conventional languages such as C, C++, etc. Despite its age, Move has its own advantages. It is developed by a more structured and professional team. Yet its age means that some flaws are still to be discovered and proven. Again, time is the best witness. Can Move rise up to be a worthy competitor of Solidity, the programming language chosen by most of the blockchain projects to write up their smart contracts, and eventually become the #1 choice for smart contract developers? It will take us quite some time before we can reach the conclusion. 

“The one who wants to wear a crown must bear the weight.”

As always, all the best to the blockchain community and looking forward to a more prosperous and mature crypto ecosystem.

By Shawn Chong

General Partner of Geekcartel

** **

Move, is it that good?

Recently, Aptos and Sui have been in the spotlight of the crypto community; among all the news, their heritage from Diem —- Move the programming language, which is now adopted by both Aptos and Sui blockchain, is the most crucial innovation for this newly created ecosystem.

Let's dive in to take a look at the most crucial things Move has to provide.

First-class resources: Move being the smart contract programming language is born to deal with digital assets. This means that it needs to possess an ability to encode the various assets and corresponding business logic that make up the financial infrastructure.

In Move, an asset is not a hash, not a string, but a specially defined code, represented by /resource/ or stored in it. Move abstracts four attributes of resources, which can be copied (copy), and is indexable (key), discardable (drop), and storable (store). Users can quickly define any resource through combinations of these four attributes. This is undoubtedly one of the many innovative features of Move. The resource-first concept is an excellent help for programmers to write safe and efficient code in a way that enhances the possibility of composability as an asset is a type by itself, which opens up a lot of possibilities in general programming. Meanwhile, in Solidity, assets are not explicitly defined, they are just treated like any other variables. 

Apart from the above-mentioned benefits, this feature makes Move more resistant to some of the known blockchain attacks such as Reentrancy. The Reentrancy attack is one of the most destructive attacks in Solidity smart contracts. A reentrancy attack occurs when a function makes an external call to another untrusted contract. Then the untrusted contract makes a recursive call back to the original function in an attempt to drain funds.

An Aptos’ medium article precisely stated the feature as “a resource can never be copied or implicitly discarded, only moved between program storage locations”, which makes it possible for Move to effectively avoid the aforementioned attack. What’s more, compared to EVM, the modular system supports cyclic recursion dependency, which makes the occurrence of the Reentrancy bug impossible. 

Next up, let’s take a close look at Move’s other important feature - Static typing.

Let’s stop here for a bit and quickly revise how we distinguish static calls from dynamic calls. In layman's terms, when a program calls another program, if the called target can only be determined during runtime, it is recognized as a dynamic call; on the contrary, if the called target can be determined before executing and cannot be changed, the call is recognized as a static call.

Move’s structure sets each function call to be static, and the developer knows exactly when to call a function. This static type system presupposes the exposure of the problem to the compilation phase, not the runtime phase, reducing the chance of a crash during runtime.

A very popular technical jargon among coders is that “Well-typed programs never get stuck”. What it is trying to say is that “If a code is type checked, then the reliability is quite high”.    Indeed, but is it worth it to design it this way to an almost extreme extent for the sake of “security”? What is the trade-off between security and creativity here?

One thing we can be sure of is that Move is not designed to be 100% static typing, as it will greatly lower its usability. In fact, we can find that Move has found its balance point between Ripple and Ethereum’s characteristics.

If we examine Ripple closely, we can see it is a decentralized financial system itself. There is no need to build any Defi projects on it. It itself is an order book, and at the same time, it restricts the types in such an extreme sense and technically does not support innovation.

With the above being said, we can see that one of Move’s potential issues is that it could limit the creativity and innovation of its adopters. For example, I might not be able to separate the ownership rights and usage rights of an NFT with Move, as there could be a lot of data I can’t access. 

Lastly, let's discuss its security feature.

Let’s ask ourselves a question, what would happen if the smart contract code we wrote contains bugs/loopholes? What are the consequences? I believe all of us have the unanimous consensus that any bugs would be intolerable, despite their severity.

You might wonder why do we see so many attacks on loopholes arise from Dapps within the Ethereum ecosystem? The answer is that since the development efficiency and scenario iterations are very fast in the Internet era, the tolerance for bugs has increased accordingly (the mentality being, as long as it is not a significant problem, we can always fix it after we ship the MVP). Besides, most blockchain developers are from the somewhat “traditional“ Web2 industry Unless the Web3 common sense “code is money” really resides with the developers, their experience and habits from working in Web2 can potentially expose projects to more security risks. 

Another way to view this issue is that the security risks of Solidity itself are mostly due to the introduction of “Gas” from Ethereum, which led to the rise of a new category of loopholes we have never encountered before. For example, the smart contract itself has no loopholes, but the attacker can adjust the gas fee to attack and halt the smart contract at some intermediate step. These problems are completely novel among traditional developers. With almost all blockchains having the gas feature, they are all vulnerable to this issue. 

With the innovation of Move Prover, Move has the ambition to fix most of the security issues once and for all, but does it have the ability to do so?

**“The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language.”**

The developers behind Move believe that traditional software is large and complex, which makes it difficult to verify the language features used even in the simplest tasks. However, Move Prover has the potential to be adopted by most Move developers.

Before we dive deeper into it, we need to understand what Formal Verification is.

According to Wikipedia, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

Basically, we list out a bunch of rules and regulations in the programming language to see if your code has violated them. This is formal verification.

Formal verification was first integrated into the circuit (CPU). Using formal verification to verify low-level programming languages such as C or C++ (low-level language) is relatively simple, as the information provided by such languages is usually a lot less abstract. Codes that can be done in 3 lines if writing with more advanced programming languages needs to be done in 30 or even 300 lines in low-level programming languages. The reason being the more abstract the code is, the more loopholes it presents. You can think of it as the more abstract the content, the more interpretation there will be. Take Solidity for example, there is no such thing as one rule fits all when it comes to the formal verification of Solidity smart contracts. The only things we can rely on when evaluating whether a program is appropriate are past experience (adding issues discovered in the past to unit test cases), the developer’s experience, and testing. In this regard, maybe it is safe to draw the conclusion that the more advanced the programming language is, the more complicated the formal verification will be. 

In that case, to what extent can the Move Prover achieve in terms of integrating Formal Verification? My guess is that it may be able to conduct some sort of very simple formal verification, but for the more complicated components, professional smart contract auditors’ assistance will be a must.

I believe that we should always consider both sides no matter how well it is presented, adhering to the spirit of exploration and questioning, which is the intention of this report too. Although Solidity has been through numerous challenges and stands till today as a smart contract programming language, it is considered a very young programming language in a broader comparison with the other more conventional languages such as C, C++, etc. Despite its age, Move has its own advantages. It is developed by a more structured and professional team. Yet its age means that some flaws are still to be discovered and proven. Again, time is the best witness. Can Move rise up to be a worthy competitor of Solidity, the programming language chosen by most of the blockchain projects to write up their smart contracts, and eventually become the #1 choice for smart contract developers? It will take us quite some time before we can reach the conclusion. 

“The one who wants to wear a crown must bear the weight.”

As always, all the best to the blockchain community and looking forward to a more prosperous and mature crypto ecosystem.

By Shawn Chong

General Partner of Geekcartel

** **