高级类型系统的可用性:Rust案例研究
The Usability of Advanced Type Systems: Rust as a Case Study
摘要:
强制执行各种正确性和安全性保证的高级类型系统--例如线性和所有权类型--在程序设计语言研究界有着悠久的历史。尽管有这样的历史,但对这些类型系统及其可用性的以人为中心的评估几乎是不存在的,经验评估仅限于在专家(即类型系统的创建者)编写的程序中测试它们的表现力。在过去的几年里,随着在流行的Rust程序设计语言中采用仿射类型和所有权的版本,这种情况已经开始改变。随着Rust的流行,各种研究开始实证评估Rust的所有权和生命周期规则的可用性,提供了有关此类类型系统可用性的定性和定量信息。他们发现,尽管Rust在实现其安全性和性能承诺方面取得了普遍成功,但这些规则具有陡峭的学习曲线,并一再被认为是采用Rust的障碍。在这份报告中,我简要介绍了线性类型和基于区域的存储管理的历史,它们直接启发了Rust的类型系统。然后,我介绍了Rust的所有权和生命周期规则,并介绍了学术研究中最先进的可用性。我讨论了为什么这些规则很难学习和应用的理论论据和经验证据,并调查了解决这些困难的现有工作。我还借鉴了HCI和CS教育社区的更广泛的工作,以建议在这一领域的未来工作。
英文摘要:
Advanced type systems that enforce various correctness and safety guarantees--such as linear and ownership types--have a long history in the Programming Languages research community. Despite this history, a human-centered evaluation of these type systems and their usability was all but absent, with empirical evaluations limited to testing their expressiveness in programs written by experts, i.e. the creators of the type system. In the past few years, this has begun to change with the adoption of a version of affine types and ownership in the popular Rust programming language. With the increase in Rust's popularity, various studies have begun empirically evaluating the usability of Rust's Ownership and Lifetime rules, providing a breadth of qualitative and quantitative information on the usability of such type systems. They found that despite Rust's general success in achieving its promise of safety and performance, these rules come with a steep learning curve and have been repeatedly cited as a barrier to adopting Rust. In this report, I provide a brief history of linear types and region-based memory management, which directly inspired Rust's type system. I then introduce Rust's Ownership and Lifetime rules, and present the state-of-the-art in academic research into their usability. I discuss both theoretical arguments and empirical evidence for why these rules are difficult to learn and apply, and survey existing work on addressing some of these difficulties. I also draw from broader works in the HCI and CS Education communities to recommend future work in this area.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。