Functional Smart Contracts
summary
Argues that blockchains benefit from pure functional design and formal methods, and shows a concrete stack: Cardano uses a proof-of-stake Ouroboros consensus, core software in Haskell and Rust, and a smart-contract platform using an extended UTxO model. Plutus code compiles to a typed lambda core (System F Omega), is verified against a semi-formal Agda/Coq-style specification, and checked by property-based tests comparing an executable prototype to the production Haskell node. A web-based Plutus Playground runs contracts on a mock chain for development.
AI-written summary · about
chapters (9)
- 0:00Functional smart contracts intro
- 4:38Blockchain as data structure
- 10:44Why FP for blockchains
- 15:03Research to Haskell code
- 21:53Account vs UTXO models
- 26:12Extended UTXO benefits
- 31:38Plutus core execution
- 36:01Haskell with Plutus
- 43:13Plutus architecture
related talks
45mMarlowe: financial contracts on Blockchain
46mApplying Continuous Formal Methods to Cardano
45mPresent & Future of Blockchain Ⅱ
28mFrom Lambda to Ledger: An Architectural Comparison of Plinth and Plutarch
08mA brief history of "smart contracts"
22mCardano: The Blockchain Advantage
32mBuilding Smart Contract Platforms
48mWhy Writing Blockchain Applications is Hard, and How FP Can Help