- The various "modes" are going to be needed either way, because side-effectful functions at the type level are a research problem that probably isn't worth the effort.
- The in the pure functional "promotable" fragment, it probably also makes sense to relax aliasing rules / have infinite number types / etc. because all the stuff is going to compile away anyways.
I hope projects like this catch on, and incentivize Rust getting a stronger type system, because the benefits will flow in both directions.
Oh wow, that's incredibly cool. (tldr: the authors of Verus, mostly university researchers, are already thinking in this direction).
I think having guardrails like this is going to incredibly important as AI code gen starts taking a bigger role. Hopefully, as a separate comment mentioned, there can be a standard created so that AI tools can learn it more easily.
- The various "modes" are going to be needed either way, because side-effectful functions at the type level are a research problem that probably isn't worth the effort.
- The in the pure functional "promotable" fragment, it probably also makes sense to relax aliasing rules / have infinite number types / etc. because all the stuff is going to compile away anyways.
I hope projects like this catch on, and incentivize Rust getting a stronger type system, because the benefits will flow in both directions.