Simplicity for Programmable Money
summary
Simplicity is a typed, combinator-based language with no recursion or function types that targets crypto scripts; it defines programs as functions between three base type forms and implements nine combinators that suffice to build adders and word operations. Formal semantics live in Coq proofs (dependent-type verification) and the repo includes a proven SHA-256 compression implementation; proven equivalence lets execution call the OpenSSL implementation as a sound optimization.
AI-written summary · about
chapters (13)
- 0:00Introduction to Simplicity
- 0:36Bitcoin script overview
- 2:23Limitations of Bitcoin script
- 4:25Designing a new language
- 5:26Simplicity types
- 7:02Core combinators
- 13:00Implementing boolean logic
- 16:45Building a bit adder
- 18:51Verifying the adder
- 20:22Ripple carry adder
- 24:14Proving adder correctness
- 35:57Real-world applications
- 37:44Questions and answers
related talks
41mConcatenative programming and stack-based languages
36mFlexible Instruction-Set Semantics via Abstract Monads
31mHomoiconicity It Is What It Is
02h 50mIntro to Type Systems and Operational Semantics
58mFast Cryptographic Code via Partial Evaluation
25mIntroducing Emily Simplifying Functional Programming
30mAnalyzing Programs with SMT Solvers
19mFormally Verifying Optimizations with Block Simulations