Simplicity: From Bitcoin Script to Arbitrary Computation

Bitcoin Script is a language that controls the spending of coins. However, there are various alternatives that strive to be better: Ethereum's Solidity can express all computable functions and allows for more introspection into spending transactions. Due to Turing completeness, static analysis is limited. Miniscript is a declarative language that corresponds to a subset of Bitcoin Script. It allows powerful static analysis, including a complete enumeration of all spending paths as well as guarantees about resource limits. The language can express at most what Bitcoin Script can express. A question arises: Can we design a language with higher expressivity, like Solidity, that has integrity and verifiability like Miniscript? Simplicity is a functional language developed by Russel O'Connor since 2015, which we hope to deploy on the Liquid network soon. It can implement powerful smart contracts, since it can express all Boolean functions. Meanwhile, it is verifiable and admits resource bounds. The language is implemented for the Coq proof assistant, which enables machine-verified proofs of arbitrary statements about a given Simplicity program. APIs in C, Rust and Haskell are in the making. In this talk, we give a general introduction to Simplicity. We explain the structure of a Simplicity program and look into how it can be used in practice. We draw parallels to Bitcoin Script and sketch a translation to Simplicity.

By Christian Lewe of Blockstream
https://btcpp2022.sched.com/event/12P73/simplicity-from-bitcoin-script-to-arbitrary-computation