Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
|
Abstract Some blockchain programs (smart contracts) have included serious security vulnerabilities. Obsidian is a new typestate-oriented programming language that uses a strong type system to rule out some of these vulnerabilities. Although Obsidian was designed to promote usability to make it as easy as possible to write programs, strong type systems can cause a language to be difficult to use. In particular, ownership, typestate, and assets, which Obsidian uses to provide safety guarantees, have not seen broad adoption together in popular languages and result in significant usability challenges. We performed an empirical study with 20 participants comparing Obsidian to Solidity, which is the language most commonly used for writing smart contracts today. We observed that Obsidian participants were able to successfully complete more of the programming tasks than the Solidity participants. We also found that the Solidity participants commonly inserted asset-related bugs, which Obsidian detects at compile time. |
BIO
Michael Coblenz is a Basili Postdoctoral Fellow at the University of Maryland. His research focuses on techniques for designing and evaluating programming languages to make software engineers more effective. In the process, he creates and evaluates programming languages. Examples include immutability in object-oriented languages (Glacier) and on strong type systems in smart contract languages (Obsidian). He holds a Ph.D. in computer science from Carnegie Mellon University. Previously, he was a Senior Software Engineer at Apple.