Reach 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 drastically raising the productivity of DApp developers. A Decentralized Application that used to take months to develop will be able to be completed in weeks.
The Reach platform provides three services via a domain-specific language (DSL) for specifying DApps and a specialized compiler that projects the specification into the complete application while performing automatic verification of correctness properties.
We represent the DApp with a generalized backend language, and we then use “connectors” to translate this backend language to the correct bytecode, while remaining faithful to the interfaces offered by actual networks. Our backend supports the ability to specify blockchain-specific functionality, where appropriate.
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.
Discord: https://bit.ly/reachondiscord (seriously, don’t tell anyone)
KEEP IN TOUCH
#️⃣ Twitter: https://twitter.com/reachlang