Yeah. I'm more a working programmer than an academic, I fundamentally can't care about the fancy theory if the tool isn't usable in real code (I'm looking at yo

Yeah. I'm more a working programmer than an academic, I fundamentally can't care about the fancy theory if the tool isn't usable in real code (I'm looking at you, `verus! { everything is here and utterly miserable to use }`). Put differently: If the "academically superior" tooling isn't good enough, I'll be sticking to testing, fuzzers and sans-I/O style architecture with deterministic simulation testing. The best thing the Rust project could do at this point is to come up with a precondition/postcondition/invariant/etc syntax that a majority of the academics agree with, with the power to express forall and exists and such. Something that is syntactically close to Rust, can be used to annotate normal code, and can be extended tool-by-tool with something that looks like standard attribute macros etc. Then get the academics to focus on the semantics and underlying verification mechanism, while the working programmer gets `debug_assert!` power out of that.