Linear typing for resource-aware programming

Smart contracts running on blockchain platforms are critical components of decentralized applications (dApps). Often, smart contracts manipulate valuable assets, so that the correctness and security of the code is a main concern. A programming error in a smart contract can lead to huge capital losses. The recently developed Move language seems to be a step forward in term of smart contracts security and correctness. Move introduces the use of linear types to represent resources (like financial assets) in the language, in a way that permits to detect at compile time common errors on the manipulation of resources. In Move, the programmer can't successfully compile a program that loses a coin or forges a copy of a coin by mistake. We provide a bird's eye comparison between Move, applied to the Sui blockchain, and Solidity, used in Ethereum, with the aim of better understanding the errors preventable by Move's linear types. Doing so, we give a clean explanation of the move semantics in Move. We formalize the operational semantics and the type system of a core subset of the Move language we call FM, which includes linear types, and we prove the language enjoys a Resource Preservation property similar to the the Resource Safety property stated and proved by Blackshear at al. for the Move bytecode. We mechanize the proofs we have done for FM with approximately 3000 lines of code in Agda, a proof assistant based on Martin-Löf intuitionistic type theory. In the formalization we clarify what does it mean to use a resource and how the type system constraining the use of variables by programmers, with linear typing, can guarantee resources are correctly used at runtime.