From glancing at https://www.andrew.cmu.edu/user/bparno/papers/verus-ghost.pd... it is more related than you think.

- 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.