In this hands-on workshop, we introduce Reach, take participants on a walkthrough of an example program, and guide them through implementing a basic DApp on their own.
Reach, a new domain-specific language for decentralized applications, provides automatic solutions to the key problems faced by blockchain developers: ensuring the smart contract is consistent with client-side software, verifying the DApp is trustworthy, and abstracting over different blockchains.
We then take a guided tutorial consisting of an example Reach program that implements a formally-verified two-party wager DApp. We explain the structure of the ~50 line Reach program and the structure of the ~50 line JavaScript frontend, and take a deep dive into properties that Reach formally guarantees.
Participants will then work through a series of exercises implementing a different DApp with a similar structure to the sample program. They will leave with concrete experience using Reach that will enable them to build their own DApp.
Prerequisites: Experience programming in JavaScript, have Docker installed to install the imag of the Reach compiler and demo. It is recommended participants download and install this image before the workshop at: http://reach.sh. Experience with formal verification or stating DApp properties is NOT required.
