3.16 How does Reach work?

It is not necessary to understand how Reach works to use it effectively, but many users are curious about how it works. The Reach compiler uses the following strategy for analysis and compiling programs:

  1. A partial evaluation of the source program that removes all function calls & compile-time values.

  2. A linearization of the residual program that removes the need for a runtime stack to track any consensus state.

  3. A conservative (sound) analysis of the knowledge of each participant.

  4. A reduction of the program to an instance of an SMT (satisfiability modulo theories) theory of decentralized applications.

  5. An end-point projection of the linearization to produce a perspective for each participant, as well as the consensus.

  6. A single-pass top-down construction of backend and consensus programs.

Reach is proud to: be implemented in Haskell using the Glorious Haskell Compiler; use the Z3 theorem prover for verification; use Racket’s Scribble tool for documentation; and use Docker for containerization.