Matthias
This week we continue with the work from last week on the pure model. We added (and described more) properties that are checked by the automatically generated tests. Furthermore, since the core of the pure model is an abstract and reusable pattern, we started to implement the DEX-specific instantiation of this pattern.
Working together with Well-Typed means that we not only get some additional work power but also will improve our way of working: Especially leveraging their experience in writing blockchain-related software. For example, as soon as the understanding of the DEX design is clear for everybody, we will transform the yet informal description into a more formal specification. This will force us to describe every state and every change of the design more clearly. So finally, it will help to verify that the pure model and, later, the on-chain code, behave as expected. Note: The on-chain code model is substantially more complex than the pure model since it needs to work in the blockchain context.
In this video, Duncan Coutts from Well-Typed describes how we will use the simple, pure model to test the correct behavior of the complex, blockchain-aware on-chain code. In essence:
- A simple input for the pure model is mapped to a complex input for the complex model.
- Then each model processes it’s input.
- The output of the complex model is mapped back to a simple model and compared with the result of the pure model.
- If the two outcomes are the same, the models are assumed to behave in the same way.
For the next week, we will continue the work on the pure model, the understanding of our chosen DEX design, and start with a more formal description of the approach.
