论文标题
高级类型系统可以使用吗?对黑曜石的所有权,资产和打字的实证研究
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
论文作者
论文摘要
一些区块链计划(智能合约)包括严重的安全漏洞。黑曜石是一种新的面向更植物的编程语言,它使用强大的类型系统来排除这些漏洞中的某些漏洞。尽管黑曜石旨在促进可用性以使其尽可能容易编写程序,但强大的系统可能会导致语言难以使用。特别是,黑曜石用来提供安全保证的所有权,典型和资产,并没有看到广泛采用流行语言,并带来了重大的可用性挑战。我们进行了一项实证研究,有20名参与者将黑曜石与坚固性进行比较,这是当今最常用的语言。我们观察到,黑曜石参与者能够成功完成更多的编程任务,而不是固体参与者。我们还发现,坚固的参与者通常插入与资产相关的错误,黑曜石在编译时检测到。
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.