Interesting. In the Rust world extensions like Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look: https://githu

Interesting. In the Rust world extensions like Verus, I think, are trying to enable exactly what the author is discussing. Perhaps worth a look: https://github.com/verus-lang/verus https://github.com/verus-lang/verus