解决新功能开发与健全性问题修复困境,Rust决定成立类型系统团队

考虑到程序语言Rust未来的发展,要在满足高安全性的前提下,继续发展更多的程序语言功能,Rust基金会规划了2023年到2027年4阶段发展计划,而这一系列的工作,从成立类型(Type)系统团队开始,该团队为语言和编译器团队的子团队,负责定义和维护Rust的类型检查器、特征求解器(Trait Solver)和借用检查器(Borrow Checker)。

Rust官方希望通过创建起类型团队,加速修复类型系统相关的健全性问题,官方提到,这些问题通常都是编译器和语言功能的边缘案例,由专门的测试人员或是白帽黑客发现,虽然一般开发者并不会遭遇到这些问题,但是官方仍想要尽快消除这些边缘案例。另外,因为编译器维护者太少,加上语言设计的贡献者缺乏对语言通盘了解,导致新语言功能发展困难,而通过专注于类型系统的团队,将有助于缓解这种处境。

类型团队具体工作,开发并维护包括类型检查器,用以松散定义变量分配其类型语义和实例的方式,还有替类型定义特征的特征求解器,甚至是用以证明Rust所有权模型始终成立的借用检查器这些在编译器rustc中所使用的类型工具。同时类型团队还要编写Rust的正式定义、类型检查器和语义,并且提供不安全程序代码指南。

类型团队的范畴很大,包含2018年就已经存在的Rust特征工作组,特征工作组目的是要创建高性能Rust特征系统,像是特征解决函数库Chalk,而由于功能的延伸,因此特征工作组的工作也波及类型检查器和借用检查器。另一个相关的则是Polonius工作组,主要设计和实例Polonius借用检查函数库,目前也被编入Rust类型团队。

官方提到,目前Rust团队正致力编写Rust规范,而拥有类型系统的范式(Formalization)定义将有助于此目标,无论之后是否会集成到更通用的规范中,范式能够更好地评估潜在新功能和健全性漏洞。

在Rust 1.0发布不久之后,Rust开发团队便开始朝此目标前进的工作,Chalk特征求解器便是初期成果,Chalk的核心思想是将Rust特征系统的语法和概念,转换成一组逻辑规则,并且可以使用类似Prolog的求解器来求解。当这组逻辑和解决方案,与编译器本身的特征求解器达到相同水准,则能够简单地替换现有求解器,同时该求解器也可以被用于其他工具。

不过由于Chalk仅是类型系统的一部分,而且编译器与范式对求解器的需求不同,因此现在Chalk不再是类型团队的发展重点,即便Chalk仍然是一个有用的实验性工具,但是在类型团队新任务规划中,他们将重点转移到模块化特征求解器,以及称为a-mir-formality的Rust类型系统范式。

类型团队2023年上半年的工作,目标让开发中的特征求解器可以进行测试,而a-mir-formality能够开始使用Rust测试组件进行测试,而在下半年,Rust预计将会以新的特征求解器,取代部分现存的特征求解器,官方希望在2027年解决所有类型健全性问题,并且a-mir-formality可以通过Rust测试组件可达99.9%。