Proof happens before compilation, and doesn't require compilation. You can follow the Verus tutorials for the specifics, but you can use it as a standalone verifier or as a compilation "stage" where it'll run its verification and then conditionally continue on to compilation.
Their tutorial seems ok: <a href="https://verus-lang.github.io/verus/guide/overview.html" rel="nofollow">https://verus-lang.github.io/verus/guide/overview.html
But if you want a more complete tutorial on this concept using similar tools (so what you learn from them will transfer well to Verus, even if you need to learn Verus or Rust specific details) check out Dafny or SPARK/Ada. The latter is mature and used in some parts of the software industry today. The former, I don't know if anyone actually uses it in production though theoretically you can (it generates code in several languages, I have not used it for that myself, just in an instructional capacity).
reddit_clone · · focus · HN ↗
I am new to Rust and also new to formal verification.
Can someone ELI5 this for me?
(Also, when does the proof happen? During compilation or by running extra tests during unit testing?)
Jtsummers · · focus · HN ↗
Their tutorial seems ok: <a href="https://verus-lang.github.io/verus/guide/overview.html" rel="nofollow">https://verus-lang.github.io/verus/guide/overview.html
But if you want a more complete tutorial on this concept using similar tools (so what you learn from them will transfer well to Verus, even if you need to learn Verus or Rust specific details) check out Dafny or SPARK/Ada. The latter is mature and used in some parts of the software industry today. The former, I don't know if anyone actually uses it in production though theoretically you can (it generates code in several languages, I have not used it for that myself, just in an instructional capacity).