From f51ebd0cd01bc08eb60d95617645d85cefe8b6e9 Mon Sep 17 00:00:00 2001 From: lcnr Date: Thu, 20 Jun 2024 12:46:58 +0200 Subject: [PATCH 1/5] types team update Co-authored-by: Jack Huey <31162821+jackh726@users.noreply.github.com> Co-authored-by: Niko Matsakis --- posts/2024-06-20-types-team-update.md | 225 ++++++++++++++++++++++++++ 1 file changed, 225 insertions(+) create mode 100644 posts/2024-06-20-types-team-update.md diff --git a/posts/2024-06-20-types-team-update.md b/posts/2024-06-20-types-team-update.md new file mode 100644 index 000000000..822f6b84f --- /dev/null +++ b/posts/2024-06-20-types-team-update.md @@ -0,0 +1,225 @@ +--- +layout: post +title: "Types Team Update and Roadmap" +author: lcnr +team: The Types Team +--- + +It has been more than a year since [the initial blog post][TypesAnnouncement] announcing the Types team, and our initial set of goals. For details on what the team is, why it was formed, or our previously-stated overarching goals, go check out that blog post. In short the Types team's purview extends to the parts of the Rust language and compiler that involve the type system, e.g. type checking, trait solving, and borrow checking. Our short and long term goals effectively work to make the type system sound, consistent, extensible, and fast. + +Before getting into details, it's worth sharing a quick point: the team over the last year has been very successful. Oftentimes, it's hard to measure impact, particularly when long-term roadmap goals are hard to quantify progress on and various short-term goals either are hit or aren't. But, there is one clear statistic that somewhat indictative of the team's progress: over the last year or so, [more than 50 user-facing changes][FCPs] have landed, each separately approved by Types Team consensus through FCP. + +The changes lie at the boundary between language design and implementation, and the Types Team (which is a subteam of both the Language and Compiler Teams) existing means that not only does the Rust Project have the bandwidth to make these decisions but we also have enough people with the knowledge and experience of the type system to make informed decisions that overall make the language better. + +## The priorities of the types team + +To evaluate our progress over the last year and our roadmap going forward, +lets start with our main priorities in order of importance. We will refer +to them during the remainder of this post. To reach our goals, we need a +a healthy group of maintainers which have the expertise and capacity to +react to issues and to implement complex changes. + +### The type system should be Sound + +One of the main promises of Rust is that there cannot be undefined behavior when using +only safe code. It might surprise you that there are currently [known type system +bugs][unsoundCAT] which break these guarantees. Most of these issues were found by people familiar with +the inner workings of the compiler by explicitly looking for them and we generally do not expect +users to encounter these bugs by accident. Regardless, we deeply care about fixing them +and are working towards a fully sound and ideally verified type system. + +### The type system should be Consistent + +The type system should be easy to reason about. We should avoid rough edges and +special-cases if possible. We want to keep both the implementation and user-facing behavior +as simple as possible. Where possible we want to consider the overall design instead of +providing local targeted fixes. This is necessary to build trust in the soundness of the +type system and allows for a simpler mental model of Rust. + +### The type system should be Extensible + +Rust is still evolving and we will be required to extend the type system to enable new +language features going forward. This requires the type system to be extensible and +approachable. The design of the language should not be adapted to work around +short-comings of its current type system implementation. We should collaborate with +other teams and users to make sure we're aware of their problems and consider possible +future extensions in our implementation and design. + +### The type system should be Fast + +We care about the compile times of Rust and want to consider the impact on compile times +of our designs. We should look for effective approaches to speed up the existing implementation, +by improving caching or adding fast paths where applicable. We should also be aware of the +compile time impact of future additions to the type system and suggest more performant +solutions where possible. + +## Updates + +We have been very active over the last year and made some significant progress. There +are also a few non-technical updates we would like to share. + +## Organizational updates + +First, a huge welcome to the two new members to team since the announcement post: [@BoxyUwU] and [@aliemjay]. [@BoxyUwU] has been doing a lot of work on const generics and made significant contributions to the design of the next generation trait solver. [@aliemjay] has been working on some very subtle improvements to opaque types - `impl Trait` - and to borrow checking. They are both invaluable additions to the team. + +We also organized another in-person Types Team meetup last October, immediately prior to EuroRust. We discussed the state of the team, looked at current implementation challenges and in-progress work, and reviewed and updated [the roadmap from the previous meetup][PrevRoadmap]. Most of this will be covered in this blog post. + +Finally, as discussed in the [RFC](https://rust-lang.github.io/rfcs/3254-types-team.html), we would like to have leads rotate out regularly, largely to help share the burden and experience of leads' work. So with that being said, [@nikomatsakis](https://github.com/nikomatsakis) is rotating out and [@lcnr](https://github.com/lcnr) is joining to co-lead alongside [@jackh726](https://github.com/jackh726/). + +## Roadmap progress and major milestones + +### The next-generation trait solver + +There has been [a lot of work][NewSolver] on the [next-generation trait solver][InitiativeRepo]. +The initiative posted [a separate update][InitiativeUpdate] at the end of last year. While +we would have liked to [stabilize its use in coherence][StabilizeNS] a few months ago, +this surfaced additional small behavior regressions and hangs, causing delays. We are working on fixing these issues and intend to merge the stabilization PR soon. We are getting close to compiling the standard library +and the compiler with the new solver enabled everywhere, after which will be able to run +crater to figure out the remaining issues. We expect there to be a long tail of minor issues +and behaviorial differences from the existing implementation, so there's still a lot to do +here. There are also open design questions which we will have to resolve before stabilizing +the new implementation. + +### Async and `impl Trait` + +We stabilized `async`-fn in traits (AFIT) and return-position `impl Trait` in +traits (RPTIIT) in version 1.79 thanks to a significant effort by [@compiler-errors] and +[@spastorino]. [@cjgillot] greatly improved the way generators, and therefore async functions, +are represented in the type system[^107421]. This allowed us to support recursive +`async`-functions without too much additional work[^117703]. + +Designing the next-generation trait solver surfaced issues and future-compatability challenges +of our type-alias `impl Trait` (TAIT) implementation using the old trait solver. We are +currently reworking the design and implementation. [@oli-obk] is spear-heading this effort. +This also impacts RPIT edge-cases, forcing us to be careful to avoid accidental breakage. +There have also been some new language design questions for TAIT, so we will likely first +stabilize associated type position `impl Trait` (ATPIT) as it avoids these language design +issues while still providing the same capabilities. + +### `a-mir-formality` + +We made limited progress on [`a-mir-formality`] over the last year, mostly +because we were able to allocate less time than expected towards this work. +We have used it as the foundation towards an intuitive approach to +coinductive traits which are necessary for many of the remaining unsound +issues. + +### Fixing soundness issues + +We fixed multiple long-standing unsound issues, see [the full list of closed issues](https://github.com/rust-lang/rust/issues?q=is%3Aissue+label%3AI-unsound+label%3AT-types+-label%3Arequires-nightly+is%3Aclosed+closed%3A%3C2024-06-20+). The most most notable of which was [#80176](https://github.com/rust-lang/rust/issues/80176). This subtle issue caused us to accept methods in trait implementations whose function signature had outlives requirements not present in the trait definition. These requirements were then never proven when calling the trait method. As there were some crates which relied on this pattern by accident, even if it their usages didn't exploit this unsoundness, we first merged a [future-compatability lint](https://github.com/rust-lang/rust/issues/105572) which we then moved to a hard error after a few versions. + +We've also spent time on [categorizing the remaining open issues][unsoundCat] and integrating +them into our longterm planning. Most of the remaining ones are blocked on the +next-generation trait solver as fixing them relies on coinductive trait semantics +and improvements to implied bounds. There are some remaining issues which can be at +least partially fixed right now, and we intend to work through them as we go. +Finally, there are some issues for which we still haven't figured out the best +approach and which require some further considerations. + +## Going forward + +We made significant progress during the last year but we are not done! This section covers our goals for the rest of 2024. For each item we also link to the project goals that we have proposed as part of the Rust Project's [experimental new roadmap process](https://blog.rust-lang.org/inside-rust/2024/05/07/announcing-project-goals.html). + +### `-Znext-solver` + +* [Next-generation trait solver project goal](https://rust-lang.github.io/rust-project-goals/2024h2/next-solver.html) + +Our biggest goal is to use the [next-generation trait solver][InitiativeRepo] +everywhere by default and to fully replace the existing implementation. We are currently +finalizing the stabilization of [its use in coherence checking][StabilizeNS]. This should +already fix multiple unsound issues and fix a lot of smaller issues and inconsistencies of +the current implementation. See the stabilization report for more details. + +We are also working on extracting its implementation into a separate library +outside of the compiler itself. We would like to share the trait solver with +rust-analyzer by the end of this year. They currently use [chalk] which is no longer +actively maintained. Using the next-generation trait solver in rust-analyzer +should result in a lot of additional testing for the solver and while also improving +the IDE experience by positively impacting performance and correctness. + +We intend to slowly roll out the solver in other areas of the compiler until we're able +to fully remove the existing implementation by the end of 2025. This switch will fix +multiple unsound issues by itself and will unblock a significant amount of future work. +It will generally cleanup many rough edges of the type system, such as associated types +in binders. There are many unsound issues which can only be fixed once we exclusively +use the new implementation. + +### `a-mir-formality` + +* [`a-mir-formality` project goal](https://rust-lang.github.io/rust-project-goals/2024h2/a-mir-formality.html) + +We intend to more actively develop `a-mir-formality` this year to use it in our design process. +Using it to model parts of the type system has already been incredibly impactful and we want +to build on that. We are working on more effective testing of `a-mir-formality` by enabling its +use for actual Rust code snippets and by adding fuzzing support. This will allow us to gain +additional confidence in our model of the type system and will guide its future development. + +We plan to fully formalize some components of the type system this year. Coherence is fairly +self-contained, very subtle, and soundness-critical. This has prevented us from making significant +improvents to it in the past. We also intend to formalize coinductive trait semantics, which are +difficult to reason about and necessary to fix many longstanding soundness issues. + +### Language changes and polonius + +* [Associated Type Position Impl Trait (ATPIT) project goal](https://rust-lang.github.io/rust-project-goals/2024h2/ATPIT.html) +* [Polonius on Nightly project goal](https://rust-lang.github.io/rust-project-goals/2024h2/Polonius.html) + +We intend to get the internal implementation of opaque types ready for the stabilization +of TAIT and APTIT this year. We are also hoping to land a significant improvements our +handling of associated types in coherence checking this year. + +Our other goal is to get [Polonius], the next generation borrow checker, available on nightly, which would put us in a position to stabilize in 2025 once we have time to do more optimization and testing. + +[polonius]: https://blog.rust-lang.org/inside-rust/2023/10/06/polonius-update.html + +We also intend to support the development of other language features, such as `async`-closures, which are part of the [async project goal](https://rust-lang.github.io/rust-project-goals/2024h2/async.html), +and `dyn`-trait upcasting, which will hopefully get stabilized in the near future. + +## Roadmap + +### EOY 2024 + +- next-generation trait solver + - stable in coherence + - used by rust-analyzer +- TAIT/APTIT stabilized +- a-mir-formality + - support for fuzzing and testing Rust snippets + - complete model of coherence and coinductive trait semantics +- full polonius implementation available on nightly + +### EOY 2025 + +- next-generation trait solver used everywhere by default +- polonius stabilized + +## EOY 2027 + +- next-generation trait solver + - support for coinduction and where-bounds on binders + - enable perfect derive +- a-mir-formality fully model soundness critical parts of Rust +- all known type system unsoundnesses fixed + + +[TypesAnnouncement]: https://blog.rust-lang.org/2023/01/20/types-announcement.html +[PrevRoadmap]: https://blog.rust-lang.org/2023/01/20/types-announcement.html#roadmap +[InitiativeUpdate]: https://blog.rust-lang.org/inside-rust/2023/12/22/trait-system-refactor-initiative.html +[InitiativeRepo]: https://github.com/rust-lang/trait-system-refactor-initiative/ +[devGuide]: https://rustc-dev-guide.rust-lang.org/solve/trait-solving.html +[`a-mir-formality`]: https://github.com/rust-lang/a-mir-formality +[FCPs]: https://github.com/rust-lang/rust/pulls?q=is%3Apr+label%3AT-types+label%3Adisposition-merge+is%3Amerged+closed%3A%3E2023-01-20+sort%3Acreated-asc+ +[NewSolver]: https://github.com/rust-lang/rust/pulls?q=is%3Apr+label%3AWG-trait-system-refactor+-label%3Arollup+is%3Amerged+closed%3A%3E2023-01-20+sort%3Acreated-asc+ +[StabilizeNS]: https://github.com/rust-lang/rust/pull/121848 +[unsoundCat]: https://github.com/orgs/rust-lang/projects/44/views/1 +[chalk]: https://github.com/rust-lang/chalk/ + +[@aliemjay]: https://github.com/aliemjay +[@BoxyUwU]: https://github.com/boxyuwu +[@compiler-errors]: https://github.com/compiler-errors +[@oli-obk]: https://github.com/oli-obk +[@spastorino]: https://github.com/spastorino +[@cjgillot]: https://github.com/cjgillot + +[^107421]: stabilized in https://github.com/rust-lang/rust/issues/107421 +[^117703]: stabilized in https://github.com/rust-lang/rust/issues/117703 From 2e1bb31397e9a8ed6b0697662aec48dc6a7b3c58 Mon Sep 17 00:00:00 2001 From: lcnr Date: Thu, 20 Jun 2024 17:59:29 +0200 Subject: [PATCH 2/5] fix typo --- posts/2024-06-20-types-team-update.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/posts/2024-06-20-types-team-update.md b/posts/2024-06-20-types-team-update.md index 822f6b84f..93f7696e5 100644 --- a/posts/2024-06-20-types-team-update.md +++ b/posts/2024-06-20-types-team-update.md @@ -165,7 +165,7 @@ difficult to reason about and necessary to fix many longstanding soundness issue * [Polonius on Nightly project goal](https://rust-lang.github.io/rust-project-goals/2024h2/Polonius.html) We intend to get the internal implementation of opaque types ready for the stabilization -of TAIT and APTIT this year. We are also hoping to land a significant improvements our +of TAIT and ATPIT this year. We are also hoping to land a significant improvements our handling of associated types in coherence checking this year. Our other goal is to get [Polonius], the next generation borrow checker, available on nightly, which would put us in a position to stabilize in 2025 once we have time to do more optimization and testing. @@ -182,7 +182,7 @@ and `dyn`-trait upcasting, which will hopefully get stabilized in the near futur - next-generation trait solver - stable in coherence - used by rust-analyzer -- TAIT/APTIT stabilized +- TAIT/ATPIT stabilized - a-mir-formality - support for fuzzing and testing Rust snippets - complete model of coherence and coinductive trait semantics From 8d024e7373ea37518a01a22ca651cd6cd7fdcb01 Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 24 Jun 2024 20:58:24 +0200 Subject: [PATCH 3/5] do not talk about "binders" --- posts/2024-06-20-types-team-update.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/posts/2024-06-20-types-team-update.md b/posts/2024-06-20-types-team-update.md index 93f7696e5..6adb46000 100644 --- a/posts/2024-06-20-types-team-update.md +++ b/posts/2024-06-20-types-team-update.md @@ -141,7 +141,7 @@ We intend to slowly roll out the solver in other areas of the compiler until we' to fully remove the existing implementation by the end of 2025. This switch will fix multiple unsound issues by itself and will unblock a significant amount of future work. It will generally cleanup many rough edges of the type system, such as associated types -in binders. There are many unsound issues which can only be fixed once we exclusively +in higher-ranked types. There are many unsound issues which can only be fixed once we exclusively use the new implementation. ### `a-mir-formality` @@ -196,7 +196,7 @@ and `dyn`-trait upcasting, which will hopefully get stabilized in the near futur ## EOY 2027 - next-generation trait solver - - support for coinduction and where-bounds on binders + - support for coinduction and (implicit) where-bounds on `for<'a>` - enable perfect derive - a-mir-formality fully model soundness critical parts of Rust - all known type system unsoundnesses fixed From fc5b58b9dd2368ad1813640997aa8182a402c623 Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 24 Jun 2024 21:07:18 +0200 Subject: [PATCH 4/5] additional review + update date --- ...team-update.md => 2024-06-25-types-team-update.md} | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) rename posts/{2024-06-20-types-team-update.md => 2024-06-25-types-team-update.md} (97%) diff --git a/posts/2024-06-20-types-team-update.md b/posts/2024-06-25-types-team-update.md similarity index 97% rename from posts/2024-06-20-types-team-update.md rename to posts/2024-06-25-types-team-update.md index 6adb46000..276fd5d9f 100644 --- a/posts/2024-06-20-types-team-update.md +++ b/posts/2024-06-25-types-team-update.md @@ -83,7 +83,7 @@ the new implementation. ### Async and `impl Trait` We stabilized `async`-fn in traits (AFIT) and return-position `impl Trait` in -traits (RPTIIT) in version 1.79 thanks to a significant effort by [@compiler-errors] and +traits (RPTIIT) in version 1.75 thanks to a significant effort by [@compiler-errors] and [@spastorino]. [@cjgillot] greatly improved the way generators, and therefore async functions, are represented in the type system[^107421]. This allowed us to support recursive `async`-functions without too much additional work[^117703]. @@ -92,9 +92,9 @@ Designing the next-generation trait solver surfaced issues and future-compatabil of our type-alias `impl Trait` (TAIT) implementation using the old trait solver. We are currently reworking the design and implementation. [@oli-obk] is spear-heading this effort. This also impacts RPIT edge-cases, forcing us to be careful to avoid accidental breakage. -There have also been some new language design questions for TAIT, so we will likely first +There are some open language design questions for TAIT, so we plan to stabilize associated type position `impl Trait` (ATPIT) as it avoids these language design -issues while still providing the same capabilities. +questions while still closing the expressiveness gap. ### `a-mir-formality` @@ -165,7 +165,7 @@ difficult to reason about and necessary to fix many longstanding soundness issue * [Polonius on Nightly project goal](https://rust-lang.github.io/rust-project-goals/2024h2/Polonius.html) We intend to get the internal implementation of opaque types ready for the stabilization -of TAIT and ATPIT this year. We are also hoping to land a significant improvements our +of TAIT and ATPIT this year. We are also hoping to land significant improvements to our handling of associated types in coherence checking this year. Our other goal is to get [Polonius], the next generation borrow checker, available on nightly, which would put us in a position to stabilize in 2025 once we have time to do more optimization and testing. @@ -182,7 +182,7 @@ and `dyn`-trait upcasting, which will hopefully get stabilized in the near futur - next-generation trait solver - stable in coherence - used by rust-analyzer -- TAIT/ATPIT stabilized +- ATPIT stabilized - a-mir-formality - support for fuzzing and testing Rust snippets - complete model of coherence and coinductive trait semantics @@ -191,6 +191,7 @@ and `dyn`-trait upcasting, which will hopefully get stabilized in the near futur ### EOY 2025 - next-generation trait solver used everywhere by default +- TAIT stabilized - polonius stabilized ## EOY 2027 From 3b038f053dd18ade1560ebf15d8f9e49478b7760 Mon Sep 17 00:00:00 2001 From: lcnr Date: Wed, 26 Jun 2024 09:08:31 +0200 Subject: [PATCH 5/5] review + update date --- ...-team-update.md => 2024-06-26-types-team-update.md} | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) rename posts/{2024-06-25-types-team-update.md => 2024-06-26-types-team-update.md} (96%) diff --git a/posts/2024-06-25-types-team-update.md b/posts/2024-06-26-types-team-update.md similarity index 96% rename from posts/2024-06-25-types-team-update.md rename to posts/2024-06-26-types-team-update.md index 276fd5d9f..a06689d46 100644 --- a/posts/2024-06-25-types-team-update.md +++ b/posts/2024-06-26-types-team-update.md @@ -7,7 +7,7 @@ team: The Types Team It has been more than a year since [the initial blog post][TypesAnnouncement] announcing the Types team, and our initial set of goals. For details on what the team is, why it was formed, or our previously-stated overarching goals, go check out that blog post. In short the Types team's purview extends to the parts of the Rust language and compiler that involve the type system, e.g. type checking, trait solving, and borrow checking. Our short and long term goals effectively work to make the type system sound, consistent, extensible, and fast. -Before getting into details, it's worth sharing a quick point: the team over the last year has been very successful. Oftentimes, it's hard to measure impact, particularly when long-term roadmap goals are hard to quantify progress on and various short-term goals either are hit or aren't. But, there is one clear statistic that somewhat indictative of the team's progress: over the last year or so, [more than 50 user-facing changes][FCPs] have landed, each separately approved by Types Team consensus through FCP. +Before getting into details, it's worth sharing a quick point: the team over the last year has been very successful. Oftentimes, it's hard to measure impact, particularly when long-term roadmap goals are hard to quantify progress on and various short-term goals either are hit or aren't. But, there is one clear statistic that is somewhat indicative of the team's progress: over the last year or so, [more than 50 user-facing changes][FCPs] have landed, each separately approved by Types Team consensus through FCP. The changes lie at the boundary between language design and implementation, and the Types Team (which is a subteam of both the Language and Compiler Teams) existing means that not only does the Rust Project have the bandwidth to make these decisions but we also have enough people with the knowledge and experience of the type system to make informed decisions that overall make the language better. @@ -76,7 +76,7 @@ we would have liked to [stabilize its use in coherence][StabilizeNS] a few month this surfaced additional small behavior regressions and hangs, causing delays. We are working on fixing these issues and intend to merge the stabilization PR soon. We are getting close to compiling the standard library and the compiler with the new solver enabled everywhere, after which will be able to run crater to figure out the remaining issues. We expect there to be a long tail of minor issues -and behaviorial differences from the existing implementation, so there's still a lot to do +and behavioral differences from the existing implementation, so there's still a lot to do here. There are also open design questions which we will have to resolve before stabilizing the new implementation. @@ -88,7 +88,7 @@ traits (RPTIIT) in version 1.75 thanks to a significant effort by [@compiler-err are represented in the type system[^107421]. This allowed us to support recursive `async`-functions without too much additional work[^117703]. -Designing the next-generation trait solver surfaced issues and future-compatability challenges +Designing the next-generation trait solver surfaced issues and future-compatibility challenges of our type-alias `impl Trait` (TAIT) implementation using the old trait solver. We are currently reworking the design and implementation. [@oli-obk] is spear-heading this effort. This also impacts RPIT edge-cases, forcing us to be careful to avoid accidental breakage. @@ -106,7 +106,7 @@ issues. ### Fixing soundness issues -We fixed multiple long-standing unsound issues, see [the full list of closed issues](https://github.com/rust-lang/rust/issues?q=is%3Aissue+label%3AI-unsound+label%3AT-types+-label%3Arequires-nightly+is%3Aclosed+closed%3A%3C2024-06-20+). The most most notable of which was [#80176](https://github.com/rust-lang/rust/issues/80176). This subtle issue caused us to accept methods in trait implementations whose function signature had outlives requirements not present in the trait definition. These requirements were then never proven when calling the trait method. As there were some crates which relied on this pattern by accident, even if it their usages didn't exploit this unsoundness, we first merged a [future-compatability lint](https://github.com/rust-lang/rust/issues/105572) which we then moved to a hard error after a few versions. +We fixed multiple long-standing unsound issues, see [the full list of closed issues](https://github.com/rust-lang/rust/issues?q=is%3Aissue+label%3AI-unsound+label%3AT-types+-label%3Arequires-nightly+is%3Aclosed+closed%3A%3C2024-06-20+). The most most notable of which was [#80176](https://github.com/rust-lang/rust/issues/80176). This subtle issue caused us to accept methods in trait implementations whose function signature had outlives requirements not present in the trait definition. These requirements were then never proven when calling the trait method. As there were some crates which relied on this pattern by accident, even if it their usages didn't exploit this unsoundness, we first merged a [future-compatibility lint](https://github.com/rust-lang/rust/issues/105572) which we then moved to a hard error after a few versions. We've also spent time on [categorizing the remaining open issues][unsoundCat] and integrating them into our longterm planning. Most of the remaining ones are blocked on the @@ -156,7 +156,7 @@ additional confidence in our model of the type system and will guide its future We plan to fully formalize some components of the type system this year. Coherence is fairly self-contained, very subtle, and soundness-critical. This has prevented us from making significant -improvents to it in the past. We also intend to formalize coinductive trait semantics, which are +improvements to it in the past. We also intend to formalize coinductive trait semantics, which are difficult to reason about and necessary to fix many longstanding soundness issues. ### Language changes and polonius