Detailed Plan
Reach will build a blockchain-enforced information trade application as a proof of concept of Reach's ability to seamlessly work with your protocol; a first step to demonstrating Reach's ability to support your platform's mission.
The Reach platform provides three essential 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.
Ease of Network Adoption
Our DSL uses a subset of JavaScript to specify the DApp at an abstract level involving potentially infinite interactions between individual participants performing finite computations over consensus data in the presence of rely-guarantee assertions. This enables us to abstract over particular blockchain networks, while remaining faithful to the interfaces offered by actual networks.
Since Reach abstracts the low-level details of the blockchain network, it enables DApp authors to develop on one platform (or purely in simulation) and deploy on another network. This is especially valuable for platforms in development that would otherwise need to onboard developers and coax them into rewriting their software to use the new system.
There are many existing DApps that are not built on Cardano and would require significant effort and energy to port. The Reach platform offers a concrete migration path via its abstract model of backend networks; this will increase day-1 adoption of Cardano.
Ease of Component Coordination
The Reach compiler uses type-checking, A Normal-Form transformation, information-flow security, and end-point projection to derive each component correctly from the single specification.
Ease of Correctness
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. Reach enables formal guarantees to be embedded in the source code and automatically verified. Auditors of Reach programs can objectively assert the correctness of DApps by adding more guarantees to the source code and demonstrating that these new properties are met (or not). Anything that increases the trustworthiness of DApps will be a boon for the blockchain community, which is reeling from the lack of confidence inspired by high-profile attacks.
In summary, Reach builds on decades of research in formal verification, compilation, and optimization of cryptographic protocols. The robustness of these aforementioned techniques will be demonstrated in the building out of the POCPoC blockchain-enforced information trade application on your platform.
Further information is in the attached document.
**YouTube Channel:** <https://www.youtube.com/reachsh>