At the intersection of Game Theory and Game Semantics, of Logic and Probabilities, of asynchronous distributed calculi and consensual sequential computations, of static proofs and dynamic reflection, of cryptographic privacy and public auditability — there is the specification and proven-correct extraction of a distributed application (dApp) where the interests of participants are kept aligned by a cryptocurrency smart contract. I will discuss the challenges that the LegiLogic team is trying to solve using Coq, as we are developing a new approach to building dApps that are correct by construction, and thereby solve scalability and interoperability issues for blockchains.

I will study your problem domain and distill its essence in a domain-specific language; around this language I can then design, implement and evolve radically simple solutions that are robust and maintainable, secure and efficient. I enjoy getting my hands dirty, but first I want to understand where we are going. I will pick the low-hanging fruits first, but as part of a plan to pick all marginally affordable fruits. I will use sound theory to achieve massive practical gains — and avoid predictable pitfalls. Many development teams have a narrow horizon that leads them to code bloat and bad quality, with diminishing returns and accumulated technical debt. Our team will keep a broad horizon to maintain a sustainable development environment. Many teams are blinded by focus on hardware devices and software artefacts and end up sacrificing the ends to the means; our team will include user experience and developer experience in our designs, and optimize the interactions that matter.