You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<h2><ahref="#formalizing-the-rust-type-system" aria-hidden="true" class="anchor" id="formalizing-the-rust-type-system"></a>Formalizing the Rust type system</h2>
90
90
<p>As mentioned above, a nearly essential element of the growing Rust language is to know how it <em>should</em> work (and to have this well documented). There are relatively recent efforts pushing for a Rust specification (like <ahref="https://github.com/ferrocene/specification">Ferrocene</a> or <ahref="https://github.com/rust-lang/rfcs/pull/3355">this open RFC</a>), but it would be hugely beneficial to have a formalized definition of the type system, regardless of its potential integration into a more general specification. In fact the existence of a formalization would allow a better assessment of potential new features or soundness holes, without the subtle intricacies of the rest of the compiler.</p>
91
91
<p>As far back as 2015, not long after the release of Rust 1.0, an experimental Rust trait solver called Chalk began to be written. The core idea of Chalk is to translate the surface syntax and ideas of the Rust trait system (e.g. traits, impls, where clauses) into a set of logic rules that can be solved using a Prolog-like solver. Then, once this set of logic and solving reaches parity with the trait solver within the compiler itself, the plan was to simply replace the existing solver. In the meantime (and continuing forward), this new solver could be used by other tools, such as rust-analyzer, where it is used today.</p>
92
-
<p>Now, given Chalk's age and the promises it had been hoped to be able to deliver on, you might be tempted to ask the question "Chalk, when?" - and plenty have. However, we've learned over the years that Chalk is likely not the correct long-term solution for Rust, for a few reasons. First, as mentioned a few times in this post, the trait solver is only but a part of a larger type system; and modeling how the entire type system fits together gives a more complete picture of its details than trying to model the parts separately. Second, the needs of the <em>compiler</em> are quite different than the needs of a <em>formalization</em>: the compiler needs performant code with the ability to track information required for powerful diagnostics; a good formalization is one that is not only complete, but also easy to maintain, read, and understand. Over the years, Chalk has tried to have both and it has so far ended up with neither.</p>
93
-
<p>So, what are the plans going forward? Well, first the types team has begun working on a formalization of the Rust typesystem, currently coined <ahref="https://github.com/nikomatsakis/a-mir-formality/">a-mir-formality</a>. An initial experimental phase was written using <ahref="https://redex.racket-lang.org/">PLT redex</a>, but a Rust port is in-progress. There's lot to do still (including modeling more of the trait system, writing an RFC, and moving it into the rust-lang org), but it's already showing great promise.</p>
92
+
<p>Now, given Chalk's age and the promises it had been hoped it would be able to deliver on, you might be tempted to ask the question "Chalk, when?" - and plenty have. However, we've learned over the years that Chalk is likely not the correct long-term solution for Rust, for a few reasons. First, as mentioned a few times in this post, the trait solver is only but a part of a larger type system; and modeling how the entire type system fits together gives a more complete picture of its details than trying to model the parts separately. Second, the needs of the <em>compiler</em> are quite different than the needs of a <em>formalization</em>: the compiler needs performant code with the ability to track information required for powerful diagnostics; a good formalization is one that is not only complete, but also easy to maintain, read, and understand. Over the years, Chalk has tried to have both and it has so far ended up with neither.</p>
93
+
<p>So, what are the plans going forward? Well, first the types team has begun working on a formalization of the Rust typesystem, currently coined <ahref="https://github.com/nikomatsakis/a-mir-formality/">a-mir-formality</a>. An initial experimental phase was written using <ahref="https://redex.racket-lang.org/">PLT redex</a>, but a Rust port is in-progress. There's a lot to do still (including modeling more of the trait system, writing an RFC, and moving it into the rust-lang org), but it's already showing great promise.</p>
94
94
<p>Second, we've begun an <ahref="https://github.com/rust-lang/types-team/issues/58">initiative</a> for writing a new trait solver in-tree. This new trait solver is more limited in scope than a-mir-formality (i.e. not intending to encompass the entire type system). In many ways, it's expected to be quite similar to Chalk, but leverage bits and pieces of the existing compiler and trait solver in order to make the transition as painless as possible. We do expect it to be pulled out-of-tree at some point, so it's being written to be as modular as possible. During our types team meetup earlier this month, we were able to hash out what we expect the structure of the solver to look like, and we've already gotten that <ahref="https://github.com/rust-lang/rust/pull/105661">merged into the source tree</a>.</p>
95
95
<p>Finally, Chalk is no longer going to be a focus of the team. In the short term, it still may remain a useful tool for experimentation. As said before, rust-analyzer uses Chalk as its trait solver. It's also able to be used in rustc under an unstable feature flag. Thus, new ideas currently could be implemented in Chalk and battle-tested in practice. However, this benefit will likely not last long as a-mir-formality and the new in-tree trait solver get more usable and their interfaces become more accessible. All this is not to say that Chalk has been a failure. In fact, Chalk has taught us a lot about how to think about the Rust trait solver in a logical way and the current Rust trait solver has evolved over time to more closely model Chalk, even if incompletely. We expect to still support Chalk in some capacity for the time being, for rust-analyzer and potentially for those interested in experimenting with it.</p>
0 commit comments