3 ms·
One of the Coq downsides is the speed. Partially because of the higher level computations, but also partially because of the OCaml. I hope, OCaml Multicore will
by xvilka 6y ago
One of the Coq downsides is the speed. Partially because of the higher level computations, but also partially because of the OCaml. I hope, OCaml Multicore will help the cause significantly.
- abhgh 6y agoWould you happen to know if the speed decreases "gracefully"? As in for a SAT/SMT problem, would Coq be at least as fast as z3?
- the-smug-one 6y agoYou would generally not use Coq to solve SAT or SMT problems, you'd use Coq to prove things. Coq will most probably not be as fast as Z3.