An Empirical Study of Ownership, Assets, and Typestate in Obsidian
summary
A new language, Obsidian, implements typestate and linearity to track ownership and prevent asset loss; authors run a randomized controlled trial with 20 participants and a compiler-based tutorial (~1.5 hours). Tasks include an auction and a prescription deposit; Obsidian participants complete the auction correctly 6 times versus 2 for Solidity, and all 6 who use ownership for prescriptions finish while most Solidity attempts need complex dynamic bookkeeping. The study claims strong static types catch real bugs and remain usable after brief training.
AI-written summary · about
chapters (20)
- 0:00Empirical Evaluation of Programming Languages
- 1:13Blockchains and Smart Contracts
- 1:33Smart Contract Security
- 1:54Design Ideas
- 2:49Without Typestate
- 3:11With Linearity
- 4:34Obsidian Example
- 7:01Quantitative Study
- 7:42Participants
- 8:04Procedure
- 8:33Tutorial
- 8:59Task Objectives
- 9:46Auction Task
- 11:19Results: Successes
- 12:25Prescription Task
- 12:51Prescription in Solidity
- 13:29Threats to Validity
- 13:46Observations
- 14:14Keys to Success
- 14:55Conclusion
related talks
25mMOVE, Enabling the Next Object Based Blockchains
42mEvidence-Oriented Programming
41mBattle of the Languages
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
17mFoundations for a Rust-Like Borrow Checker for C
24mRay Internals: Object Management with the Ownership Model
24mImperative Quantum Programming with Ownership and Borrowing in Guppy
31mIs there a use for linear types?