Re:Proofs and Refutations Using Z3
by colanderman on Friday February 16, 2018 @10:41AM
(#16393067)
Proof assistants are not magically bug-free.
As others have said, an exhaustive model checker failing to find a counterexample is a proof. That you trust proofs more because you haven't yet seen a bug in a proof assistant speaks only to your personal experience, not to any logical truism.
(That said, most models are not finite, and thus cannot be exhaustively checked. This is where proof systems do have a leg up. But that has nothing to do with bugs or representation of the system under test.)
As others have said, an exhaustive model checker failing to find a counterexample is a proof. That you trust proofs more because you haven't yet seen a bug in a proof assistant speaks only to your personal experience, not to any logical truism.
(That said, most models are not finite, and thus cannot be exhaustively checked. This is where proof systems do have a leg up. But that has nothing to do with bugs or representation of the system under test.)