Designs for the L4 Contract Programming Language Based on Deontic Modal Logic
Duration: 00:18:50
Speaker: Dr. Virgil Griffith & Vikram Verma
Type: Talk
Expertise: Advanced
Event: Devcon
Date: Jun 2026
We propose the creation of a domain-specific-language (DSL) for (smart) contracts are consistent, correct, and complete. Our DSL, L4, doesn’t simply fill templates, it fulfills the Curry–Howard correspondence between computer programs and mathematical proofs, i.e., what functional languages do for the 𝜆-calculus, the DSL will do for the deontic modal μ-calculus. This means the DSL natively expresses obligations, permissions, prohibitions, and other contractual concepts in a way that computers can easily reason about. The compiler will be responsible for static analysis of the contracts and automated detection of several classes of errors, including: inconsistency, inompleteness, goal satisfaction, and policy compliance. Functional languages are well-suited for this kind of formal verification, and we developing L4 in Haskell. L4 derives from the academic literature on contract formalization, everything is opensource and we invite feature requests and contributors to define and create what will become "SQL for contracts".
