This January, cryptocurrency experts gathered at Stanford University for the Blockchain Protocol Analysis and Security Engineering 2018 conference (BPASE ‘18) to discuss formal methods, empirical analysis, and risk modeling in blockchain protocols. One of the speakers was Dr. Russell O’Connor of Blockstream, who presented his Simplicity programming language, initially announced last fall.
Simplicity is a new low-level language based on the Sequent Calculus that allows user-defined smart contracts to be evaluated on a public blockchain. Whereas some existing scripting languages face the dangers of denial-of-service attacks and hacks, Simplicity has been designed to avoid them while also improving privacy through its use of Merklized Abstract Syntax Trees (MAST).
In his BPASE talk, O’Connor describes these advantages before diving into the heart of Simplicity. He talks about its denotational semantics, where a type system of just nine combinators allows for easy reasoning using off-the-shelf proof assistants; and he overviews its operational semantics, where an abstract machine designed for evaluating Simplicity programs defines their time and space costs.
As O’Connor notes, there are real challenges for cryptocurrency smart contracts because they need “to manage millions of dollars on a one-off piece of code that will only be run once and that has to execute in the adversarial environment of a public blockchain.” He believes that designing a language supporting formal verification from the beginning is the best way to conquer them.
You can now view the complete BPASE ‘18 Simplicity seminar online and read more details in O’Connor’s paper, “Simplicity: A New Language for Blockchains”.