devcon 2 / designs for the l4 contract programming language based on deontic modal logic
- YouTube
- IPFS
- Details
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: Invalid Date
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".
- Related
Devcon
Talk
25:17
Ethereum in 25 Minutes
Ethereum Foundation Chief Scientist, Vitalik Buterin, describes Ethereum.
Devcon
Talk
14:40
Backfeed
Matan Field presents on Backfeed (http://backfeed.cc), which develops resilient technology and new economic models to support free, large-scale, systematic collaboration.
Devcon
Talk
16:40
devp2p
Ethereum's Alex Leverington presents on "devp2p", Ethereum's networking protocol.
Devcon
Talk
13:54
Ethereum Blockchain Initiatives at Thomson Reuters
Tim Nugent will discuss some of Thomson Reuters’ proof-of-concept projects including oracle services providing real-time market and reference to smart contracts.
Devcon
Talk
16:18
Agreement Making in Solidity: A Legal Perspective
Bill Marino of Cornell Tech presents on Agreement Making in Solidity: A Legal Perspective.
Devcon
Talk
23:22
The Shape of Protocols to Come
Ethereum defies easy categorization—it blends aspects of money, nations, and more, yet doesn't fit neatly into any single category. To build better mental models for understanding Ethereum, we've spent the past two years stepping back and exploring the broader class it belongs to: Protocols. This talk explores the fundamental properties of protocols, strategies for navigating them, and how Ethereum can uniquely contribute to this emerging research field.
Devcon
Talk
26:09
Cultivating the Understory : Building Resilient DAOs
Let's explore the overlooked "understory" of DAOs and teams: the human layer that forms the foundation of successful decentralized governance. While much attention is given to the technical and structural aspects of DAOs (the "overstory"), we'll dive into the cultural, social, and distributed leadership elements that are crucial for the longevity and effectiveness of anything we build. Themes: DAO Ecology, Decentralized leadership, Coding culture DNA, Biomimicry for Governance
Devcon
Talk
Onchain Capital Allocation: From current mechanisms to future possbilities
Capital allocation, from paying bills to complex organizational funding, often suffers from inefficiencies and lack of transparency. Web3 has the potential to revolutionize this by enabling more efficient, effective, and transparent capital distribution. By addressing coordination failures and introducing new onchain strategies, crypto could transform how society allocates resources. Gitcoin founder Kevin Owocki will articulate this design space in this 20 minute talk.
Devcon
Breakout
07:57
The paradox of centralized tools doing accounting for decentralized finance
This talk is going to be about a paradox that has been prevalent since the early days of Cryptocurrencies. Cryptocurrencies were made to empower the individual, to be their own bank and to enable financial freedom without having to rely on centralized institutions. The paradox lies in the contradiction that when people want to do accounting or analytics for this new financial system they happily turn to centralized tools. This act enforces the status quo of finance being managed by centralized platforms and goes against the spirit of decentralization, undermining everything we are building. The talk will present multiple examples of this paradox in the world around us, from the way people do analytics (Blockfolio e.t.c.), to the way they do tax accounting (Bitcoin Tax e.t.c.). There will be some theorizing on why this is the case and underline why this is bad for the ecosystem and exceptionally dangerous for the people who utilize such services. Finally potential solutions to this problem will be presented, showing how a tool that performs decentralized financial analytics, accounting and tax reporting should look like in order to respect user's privacy and fit in this new era of decentralized finance we are now entering.
Devcon
Lightning Talk
17:37
Common Knowledge Machines
Common knowledge is a precondition for collective action. Yet, increasing polarization in information ecosystems risks undermining common knowledge formation. This talk introduces Community Posts, a mechanism that leverages diversification and zero-knowledge proofs to help people identify divides, bridge them and find common ground, fostering greater common knowledge in social networks.