Resources: A Safe Language Abstraction for Money
Authors:
Sam Blackshear,
David L. Dill,
Shaz Qadeer,
Clark W. Barrett,
John C. Mitchell,
Oded Padon,
Yoni Zohar
Abstract:
Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that manage and transfer assets, yet provide strong protection against sophisticated attacks. Addressing this need, we present flexible and reliable abstr…
▽ More
Smart contracts are programs that implement potentially sophisticated transactions on modern blockchain platforms. In the rapidly evolving blockchain environment, smart contract programming languages must allow users to write expressive programs that manage and transfer assets, yet provide strong protection against sophisticated attacks. Addressing this need, we present flexible and reliable abstractions for programming with digital currency in the Move language [Blackshear et al. 2019]. Move uses novel linear [Girard 1987] resource types with semantics drawing on C++11 [Stroustrup 2013] and Rust [Matsakis and Klock 2014]: when a resource value is assigned to a new memory location, the location previously holding it must be invalidated. In addition, a resource type can only be created or destroyed by procedures inside its declaring module. We present an executable bytecode language with resources and prove that it enjoys resource safety, a conservation property for program values that is analogous to conservation of mass in the physical world.
△ Less
Submitted 23 July, 2020; v1 submitted 10 April, 2020;
originally announced April 2020.
