consistent capitalization

Author: lqd

posts/inside-rust/2023-09-29-polonius-update.md

@@ -7,11 +7,11 @@ team: The Polonius Working Group <https://www.rust-lang.org/governance/teams/com
 
 This post lays out a roadmap to try to get Polonius on stable by Rust 2024. It identifies some high-level milestones and summarizes the key goals, as well as the recent progress.
 
-## Background on polonius
+## Background on Polonius
 
-Polonius refers to a few things. It is a [new formulation](http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/) of the borrow check. It is also a [specific project](https://github.com/rust-lang/polonius) that implemented that analysis, based on datalog. Our current plan does not make use of that datalog-based implementation, but uses what we learned implementing it to focus on reimplementing polonius within rustc.
+Polonius refers to a few things. It is a [new formulation](http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/) of the borrow check. It is also a [specific project](https://github.com/rust-lang/polonius) that implemented that analysis, based on datalog. Our current plan does not make use of that datalog-based implementation, but uses what we learned implementing it to focus on reimplementing Polonius within rustc.
 
-The motivating example for polonius is the so-called ["Problem Case #3: conditional control flow across functions"](https://github.com/rust-lang/rfcs/blob/master/text/2094-nll.md#problem-case-3-conditional-control-flow-across-functions): here, returning a reference out of a function, from a conditional.
+The motivating example for Polonius is the so-called ["Problem Case #3: conditional control flow across functions"](https://github.com/rust-lang/rfcs/blob/master/text/2094-nll.md#problem-case-3-conditional-control-flow-across-functions): here, returning a reference out of a function, from a conditional.
 
 ```rust=
 fn get_default<'r, K: Hash + Eq + Copy, V: Default>(
@@ -54,7 +54,7 @@ fn main() {
 
 Here, the loan created on iteration N _may be used_ in the `None` path on iteration N+1, however the borrowed variable at that iteration is not the same.
 
-Issues like "NLL problem case #3", issue #47680 and others, were therefore deferred from NLLs, and left as future work, [polonius](http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/).
+Issues like "NLL problem case #3", issue #47680 and others, were therefore deferred from NLLs, and left as future work, [Polonius](http://smallcultfollowing.com/babysteps/blog/2018/04/27/an-alias-based-formulation-of-the-borrow-checker/).
 
 The key ideas being:
 - switching from a model of _lifetimes_ as sets of points in the CFG (with _outlives_ relationships), to a model of _origins_ as sets of loans (with _subset_ relationships).
@@ -75,14 +75,14 @@ Here are the roadmap's milestones:
 
 Today, the trait solver produces higher-ranked outlives constraints and the borrow checker solves them. In the future, we would like to make the [next trait solver](https://github.com/rust-lang/trait-system-refactor-initiative/) responsible for solving these higher-ranked constraints itself, so that it only produces constraints on regions in the root [universe](https://rustc-dev-guide.rust-lang.org/borrow_check/region_inference/placeholders_and_universes.html#what-is-a-universe) (which the borrow checker can easily process). This would allow us to solve implication predicates like `for<T> { if (T: 'a, 'a: 'b) { T: 'b } }` without having to effectively reproduce the same trait solving logic again.
 
-In the shorter term, we can refactor the borrow checker to separate out the higher-ranked processing from the ordinary processing. The goal would be to preprocess the outlives constraints in a kind of polonius ["leak check"](https://rustc-dev-guide.rust-lang.org/traits/hrtb.html#basic-matching-and-placeholder-leaks), where we can compute the higher-ranked errors. This can then be removed once the trait solver can solve these constraints.
+In the shorter term, we can refactor the borrow checker to separate out the higher-ranked processing from the ordinary processing. The goal would be to preprocess the outlives constraints in a kind of Polonius ["leak check"](https://rustc-dev-guide.rust-lang.org/traits/hrtb.html#basic-matching-and-placeholder-leaks), where we can compute the higher-ranked errors. This can then be removed once the trait solver can solve these constraints.
 
 Current status: ⏳ members of the types team are starting to work on this task in the next few days.
 
 
 ### 2. Location-insensitive loans in scope
 
-Out of the two key differences between polonius and the existing borrow check (regions as "sets of loans", and computing subtyping relations at each point in the CFG), this step is aimed at resolving the *first* difference, but not the second, so we call it the "location *in*sensitive loans in scope" (because subtyping is being done once, not per location): the idea can be described as "NLLs with the polonius model".
+Out of the two key differences between Polonius and the existing borrow check (regions as "sets of loans", and computing subtyping relations at each point in the CFG), this step is aimed at resolving the *first* difference, but not the second, so we call it the "location *in*sensitive loans in scope" (because subtyping is being done once, not per location): the idea can be described as "NLLs with the Polonius model".
 
 Note that other aspects of the existing borrow checker are still flow-sensitive. 
 
@@ -92,7 +92,7 @@ Importantly, this change paves the way for adding location sensitivity (sets of
 
 Current status: ✅ we have completed prototypes, and have [an open PR](https://github.com/rust-lang/rust/pull/113218) to land this under a `-Z` flag, which should happen in the near future.
 
-### 3. Verify full test suite passes with location-insensitive polonius
+### 3. Verify full test suite passes with location-insensitive Polonius
 
 That PR does pass the full 15000+ tests in our suite, but we haven't yet checked on the crates published on crates.io with a crater run.
 
@@ -101,7 +101,7 @@ Compared to our internal test suite, the vast majority of published crates are e
 Current status: ⏳ in-progress, should be finalized right when the PR is just ready to land.
 
 
-### 4. Replace parts of the borrow checker with location-insensitive polonius
+### 4. Replace parts of the borrow checker with location-insensitive Polonius
 
 
 The prototype only does additional work, and does not modify the existing analysis. 
@@ -122,9 +122,9 @@ At this point it can still be inefficient, and use the feature flag, but this is
 
 Current status: we're in the design phase here, to adapt our datalog prototype and algorithms to rustc, imagining alternative ways to compute and propagate the subset constraints along the CFG.
 
-### 6. Model borrow checking and polonius in a-mir-formality
+### 6. Model borrow checking and Polonius in a-mir-formality
 
-The types team is building a model of Rust's MIR and trait system called [`a-mir-formality`][]. Once it reaches a sufficiently complete status, the intent is that the model will always be extended to cover new language features prior to stabilization. We are therefore working to add polonius into the model. This will in fact be the second time doing such modeling, as we already added polonius to a previous incarnation of a-mir-formality. In fact, that modeling work is what gave us the insights that enabled the location-insensitive polonius formulation now landing on nightly.
+The types team is building a model of Rust's MIR and trait system called [`a-mir-formality`][]. Once it reaches a sufficiently complete status, the intent is that the model will always be extended to cover new language features prior to stabilization. We are therefore working to add Polonius into the model. This will in fact be the second time doing such modeling, as we already added Polonius to a previous incarnation of a-mir-formality. In fact, that modeling work is what gave us the insights that enabled the location-insensitive Polonius formulation now landing on nightly.
 
 [`a-mir-formality`]: https://github.com/rust-lang/a-mir-formality
 
@@ -138,7 +138,7 @@ If a similar experience to NLLs in edition 2018 is to be expected again, another
 
 At this point, the location-sensitive pass is hopefully efficient enough, tested in practice, somewhat formally verified, and can be enabled in edition 2024.
 
-Around this time, librarification efforts can also be rebooted, to turn the in-tree polonius into a library, maybe using [Stable MIR][]. This is so that it could be reused elsewhere, for example in [rust-analyzer][], or [gccrs][], or by researchers working on verification tools (like [kani][]), [prusti][] and [creusot][]).
+Around this time, librarification efforts can also be rebooted, to turn the in-tree Polonius into a library, maybe using [Stable MIR][]. This is so that it could be reused elsewhere, for example in [rust-analyzer][], or [gccrs][], or by researchers working on verification tools (like [kani][]), [prusti][] and [creusot][]).
 
 [Stable MIR]: https://github.com/rust-lang/team/pull/729
 [rust-analyzer]: https://github.com/rust-lang/rust-analyzer
@@ -149,4 +149,4 @@ Around this time, librarification efforts can also be rebooted, to turn the in-t
 
 ## Conclusion
 
-We are very excited to see the plan for polonius coming into focus. At the moment, as we are still doing foundational work, we are not looking for volunteers or contributors unless they are well versed in the compiler. We do expect that as the project proceeds, there will be more and more need for new contributions. Stay tuned for updates!
+We are very excited to see the plan for Polonius coming into focus. At the moment, as we are still doing foundational work, we are not looking for volunteers or contributors unless they are well versed in the compiler. We do expect that as the project proceeds, there will be more and more need for new contributions. Stay tuned for updates!