How It Works

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.

Why

1

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.

2

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.

3

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.

How

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.

icon
icon

High-Level Language

We allow the developer to write and think at the level of business logic, rather than at the level of the intricate details of a blockchain protocol. Our DSL uses a subset of JavaScript to specify the entire DApp: the smart contract, the clients run on the front-end, the servers run on the back-end, and all communication between all the pieces. Since the entire specification is in a single language, we enable any developer to quickly create, reason about and deploy DApps.

icon
icon

Blockchain Agnostic

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.

icon
icon

Safety Guarantees

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.

Ready to make blockchain practical?