Whenever proof tools are brought up, I tend to wonder how one goes from the proofs as written to actual code that can run in production in a way that guarantees the proof holds - how does that happen?
The linked page even says "It’s the software equivalent of a blueprint" - how does one go from that blueprint to something that functions?
The linked page even says "It’s the software equivalent of a blueprint" - how does one go from that blueprint to something that functions?