Interview
summary
Building a new blockchain language that targets smart contracts and gives statically verifiable costs, with the goal of proving correctness because contracts get one shot to be right. Uses a proof assistant (uploader notes Coq) to formalize and verify functional programs written in the language and demos a verified example, showing the approach works end to end. Advocates dependently typed programming to merge code and proofs for practical onchain reasoning.
AI-written summary · about
chapters (4)
- 0:00Start
- 0:24What are you building and what's the coolest thing about it?
- 1:21What kind of best practices are you going to share?
- 1:42What kind of best practices are you hoping to learn?
related talks
48mWhy Writing Blockchain Applications is Hard, and How FP Can Help
18mFormalising Decentralised Exchanges in Coq
30mConstructing Trustworthy Smart Contracts
29mCompositional Verification of Smart Contracts Through Communication Abstraction
23mGradual Verification for Smart Contracts
23mUsing LLM Generated Formal Specs to Prevent the Next DeFi Hack
38mAutomatically Synthesising Programs that We Can Trust
30mMulti-language Runtime Environments for Smart Contract Execution