That's fascinating. Does it mean it verifies mathematical proofs directly within the Rust code? Does anyone know the underlying principles of how this is possible?
<a href="https://verus-lang.github.io/verus/publications-and-projects/" rel="nofollow">https://verus-lang.github.io/verus/publications-and-projects... - The papers here go into their implementation. They take the proof statements and information about the program and turn it into an SMT problem (and run it through Z3 if I read correctly) and then they use that to prove the properties of the program.
SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.
<a href="https://mitpress.mit.edu/9780262546232/program-proofs/" rel="nofollow">https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic
<a href="https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html#" rel="nofollow">https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
jdw64 · · focus · HN ↗
Jtsummers · · focus · HN ↗
SPARK/Ada and Dafny work similarly, and have good documentation if you want to try your hand at something with a (presently) better set of documentation.
<a href="https://mitpress.mit.edu/9780262546232/program-proofs/" rel="nofollow">https://mitpress.mit.edu/9780262546232/program-proofs/ - Dafny book, pretty good tutorial on the topic
<a href="https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html#" rel="nofollow">https://learn.adacore.com/courses/intro-to-spark/chapters/01... - Free tutorial for SPARK
jdw64 · · focus · HN ↗