3 ms·
I'm not sure why the example used for formal verification is Z3, and not proof assistants like Coq or Agda. SMT solvers have made verification a lot more access
by smasher164 5y ago
I'm not sure why the example used for formal verification is Z3, and not proof assistants like Coq or Agda. SMT solvers have made verification a lot more accessible, but Coq is strictly more expressive than Z3.
- ebingdom 5y agoCoq requires thinking like a functional programmer, and most programmers are resistant to that paradigm for some reason.