> You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.
Agreed, though I think Lean is making big progress in the UX front of ITP verification through its extensive meta-programming facilities.
My issue with these tools applied to verifying external languages like Rust, is that the proof is not written in the target language, forcing your developers to learn two languages.
I have recently been thinking about what a "verification aware Rust" would look like, colored by my experience writing Creusot, the work on Verus and Aeneas and my time in the lab developing Why3. I think building such a language from the ground up could provide a step change in ease of verification even from Rust, particularly with regard to those "hard parts" of the proof.
Agreed, though I think Lean is making big progress in the UX front of ITP verification through its extensive meta-programming facilities.
My issue with these tools applied to verifying external languages like Rust, is that the proof is not written in the target language, forcing your developers to learn two languages.
I have recently been thinking about what a "verification aware Rust" would look like, colored by my experience writing Creusot, the work on Verus and Aeneas and my time in the lab developing Why3. I think building such a language from the ground up could provide a step change in ease of verification even from Rust, particularly with regard to those "hard parts" of the proof.