We believe that blockchains have not reached their full potential because no development environment provides these services. Therefore, developers must provide for them on their own, which is expensive and error-prone.The Reach platform will enable tens of millions of developers to participate in the Blockchain community, rather than only the thousands that participate today, by drastically lowering the barrier to entry into blockchain and seriously raising the productivity of DApp developers.
Traditional developers are not included in the blockchain movement today.
Current blockchain development requires detailed knowledge of particular networks and cryptographic techniques. This knowledge is not pervasive among traditional full-stack developers. Further, it is too expensive and risky to acquire because no blockchain platform is perceived as “safe” or dominant.
DApps involve many cooperating components to deploy successfully and safely.
The details of the smart contract, front-ends, and correctness proofs must all agree on every detail of the program from the protocol details (like data formats and method API) to the logical operations of the program. No existing DApp language allows all of these components to be specified at the same time or in a way that guarantees consistency.
DApps require a high standard of correctness because mistakes can automatically put great financial resources at risk (c.f. DAO hack).
No existing DApp development environment incorporates formal verification of the distributed computation executed by the DApp.
The Reach platform provides these three services via a domain-specific language (DSL) for specifying DApps and a specialized compiler that projects the specification into each of the output components while performing automatic verification of correctness properties.
We output the DApp to a generalized backend language, and we then use “connectors” to translate the backend language to the correct byte code, while remaining faithful to the interfaces offered by actual networks. This allows a developer to build on any blockchain platform that would best serve the DApp.
We ensure that the DApp is free from errors without having to write tests of what the program should do. Instead, developers write down what their program must not do, and we ensure that these bad outcomes never occur. The compiler uses type-checking, A Normal-Form transformation, information-flow security, and end-point projection to derive each component correctly from the single specification. The compiler is integrated with a satisfiability-modulo-theories (SMT) theorem prover (e.g. Z3) to automatically check the correctness of the application via developer-specific predicates, as well as automatically generated properties appropriate for all DApps.