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