Simplicity for Programmable Money

Imagine taking your favourite functional programming language and removing recursion, recursive types, and even removing function types. What do you have left? Everything you need for programmable money! Simplicity is a new typed, combinator-based, functional language without loops and recursion, designed to be used within crypto-currencies and blockchain applications. Simplicity comes with formal semantics defined using Coq, a popular, general purpose software proof assistant based on dependent type theory. In this presentation I will describe the Simplicity language. I will demonstrate how to write some small programs in Simplicity and show how to use prove that they behave correctly with some live coding. For more information on Simplicity see https://github.com/ElementsProject/simplicity .