So enthused that this is public now! Great work. Sent from my iPhone
> On Oct 30, 2017, at 8:22 AM, Russell O'Connor via bitcoin-dev > <bitcoin-dev@lists.linuxfoundation.org> wrote: > > I've been working on the design and implementation of an alternative to > Bitcoin Script, which I call Simplicity. Today, I am presenting my design at > the PLAS 2017 Workshop on Programming Languages and Analysis for Security. > You find a copy of my Simplicity paper at > https://blockstream.com/simplicity.pdf > > Simplicity is a low-level, typed, functional, native MAST language where > programs are built from basic combinators. Like Bitcoin Script, Simplicity > is designed to operate at the consensus layer. While one can write > Simplicity by hand, it is expected to be the target of one, or multiple, > front-end languages. > > Simplicity comes with formal denotational semantics (i.e. semantics of what > programs compute) and formal operational semantics (i.e. semantics of how > programs compute). These are both formalized in the Coq proof assistant and > proven equivalent. > > Formal denotational semantics are of limited value unless one can use them in > practice to reason about programs. I've used Simplicity's formal semantics to > prove correct an implementation of the SHA-256 compression function written > in Simplicity. I have also implemented a variant of ECDSA signature > verification in Simplicity, and plan to formally validate its correctness > along with the associated elliptic curve operations. > > Simplicity comes with easy to compute static analyses that can compute bounds > on the space and time resources needed for evaluation. This is important > for both node operators, so that the costs are knows before evaluation, and > for designing Simplicity programs, so that smart-contract participants can > know the costs of their contract before committing to it. > > As a native MAST language, unused branches of Simplicity programs are pruned > at redemption time. This enhances privacy, reduces the block weight used, > and can reduce space and time resource costs needed for evaluation. > > To make Simplicity practical, jets replace common Simplicity expressions > (identified by their MAST root) and directly implement them with C code. I > anticipate developing a broad set of useful jets covering arithmetic > operations, elliptic curve operations, and cryptographic operations including > hashing and digital signature validation. > > The paper I am presenting at PLAS describes only the foundation of the > Simplicity language. The final design includes extensions not covered in the > paper, including > > - full convent support, allowing access to all transaction data. > - support for signature aggregation. > - support for delegation. > > Simplicity is still in a research and development phase. I'm working to > produce a bare-bones SDK that will include > > - the formal semantics and correctness proofs in Coq > - a Haskell implementation for constructing Simplicity programs > - and a C interpreter for Simplicity. > > After an SDK is complete the next step will be making Simplicity available in > the Elements project so that anyone can start experimenting with Simplicity > in sidechains. Only after extensive vetting would it be suitable to consider > Simplicity for inclusion in Bitcoin. > > Simplicity has a long ways to go still, and this work is not intended to > delay consideration of the various Merkelized Script proposals that are > currently ongoing. > _______________________________________________ > bitcoin-dev mailing list > bitcoin-dev@lists.linuxfoundation.org > https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
_______________________________________________ bitcoin-dev mailing list bitcoin-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
