STstaticassertion·Jun 22, 2020
Sorry that I see your post is downvoted, I'm generally in agreement, as an avid rust programmer. Rust can express a lot of safety guarantees, but there's a massive amount of room for improvements, and I'm sorry that the community hasn't been accepting of that in your interactions.
> Similarly, state machine formal verification to prevent design bugs are something that hardware engineers are deeply aware of but would also be extremely useful to ensure "correct-by-construction" event driven code.
This reminds me a lot of P. Rust has a crate that I wouldn't necessarily recommend, but it might be similar to what you want:
https://github.com/fitzgen/state_machine_future
Of course, in this case the code is the model, there is no verification here.
The Z3 integration with Nim is super cool, would love to see something like that for Rust. I know
Read the rest
of some existing research that reminds me of this but I don't have time to dig up the paper - it was implemented in macros, and looked a lot like what you've got there, with pre/post conditions, ensures, etc. If someone has that paper, please link it! I would love to reread.
edit: Here's one rust crate leveraging Z3, but not the one I was thinking of
https://github.com/Rust-Proof/rustproof