高级类型系统能否好用？对 Obsidian 中所有权、资产与类型状态的实证研究

一些区块链程序（智能合约）曾包含严重的安全漏洞。Obsidian 是一种新的面向类型状态的编程语言，它使用强类型系统来排除其中部分漏洞。尽管 Obsidian 旨在提升可用性，以尽可能轻松地编写程序，但强类型系统可能导致语言难以使用。特别是，Obsidian 用于提供安全性保证的所有权、类型状态和资产，在流行语言中尚未被共同广泛采用，并带来了显著的可用性挑战。我们对 20 名参与者进行了实证研究，将 Obsidian 与当今最常用于编写智能合约的语言 Solidity 进行比较。我们观察到，Obsidian 参与者比 Solidity 参与者成功完成了更多的编程任务。我们还发现，Solidity 参与者普遍插入了与资产相关的错误，而 Obsidian 在编译时即可检测这些错误。