The Rust team will work on formalizing its type system under a process expected to be complete by the end of 2027, according to a post on the official site about and from the recently formed Types team.
Although Rust is among the safest and most reliable programming languages, it lacks a formal specification, something that has been less problematic than one might expect because of the close relationship between Rust and its compiler rustc. As this proposal for a specification puts it:
“Unlike the C or C++ standard, the Rust specification does not provide a set of requirements for a compiler to be able to call itself ‘a Rust™ compiler’. Instead, it specifies the behaviour of the Rust compiler.”
Even so, the Rust team is conscious of the lack and the new post states that “it would be hugely beneficial to have a formalized definition of the type system, regardless of its potential integration into a more general specification.” An early approach to this, called Chalk, was designed to be a “trait solver”. A Rust trait, somewhat but not completely similar to an interface in other languages like Java and C#, is a fundamental concept in the language. The team though has now decided that Chalk was trying to do two things at once: to be used by the compiler but also to be “easy to maintain, read, and understand.”
“Chalk is no longer going to be a focus of the team,” says the new post, though it will still “remain a useful tool for experimentation.” The new focus will be on two separate pieces, a modular trait solver for one purpose, and for the other a formalization of the Rust type system called a-mir-formality, a punning name that references MIR or Mid-level Intermediate Representation, a simplified form of Rust used for safety checks, optimization and code generation.
Aside from other benefits, one reason for focusing on the type system is to fix “soundness bugs in the language relating to the type system.” There are currently 62 open unsoundness issues though we are assure that “in practice these will not pop up in the programs you write,” as they are edge cases.
The team nevertheless aims to fix these issues and has set out a roadmap for the new trait solver as well as for a-mir-formality and for fixing type-related unsound issues, concluding in 2027 when “a-mir-formality passes 99.9% of the Rust test suite.”
Nikio Matsakis on the Rust Language team has also posted about the “maturation and scaling” of Rust, listing “beginning work on a Rust specification” as a priority for 2023, among other goals. “It’s clear that the experience of Rust developers could be a lot smoother,” said Matsakis, suggesting that a priority is to improve the developer experience of this language that is admired but often considered difficult to learn.