I already do, my tool produces WhyML modules from Rust crates. But we can leverage Rust's ownership typing to drastically reduce proof obligations related to pointers and memory.
Incidentally, I've started working on a VSCode frontend to Why3 to replace the existing GTK one (https://github.com/xldenis/whycode), I'm currently rewriting the PoC as an LSP extension.
More broadly in the context of a Frama-Rust, much like Frama-C Why3 would be one of many possible backends. I specifically want abstract interpreters, test generation and other analyses to integrate and co-operate to solve proof obligations.
Ie: abstract interpretation could infer a loop invariant which is then used by a deductive backend to prove the function contract. Or a deductive failure could produce a counterexample which is transformed into a test case automatically.
Incidentally, I've started working on a VSCode frontend to Why3 to replace the existing GTK one (https://github.com/xldenis/whycode), I'm currently rewriting the PoC as an LSP extension.
More broadly in the context of a Frama-Rust, much like Frama-C Why3 would be one of many possible backends. I specifically want abstract interpreters, test generation and other analyses to integrate and co-operate to solve proof obligations.
Ie: abstract interpretation could infer a loop invariant which is then used by a deductive backend to prove the function contract. Or a deductive failure could produce a counterexample which is transformed into a test case automatically.