2 ms·

I'm not super informed about this but never thought of Z3 and Coq as even being related. As far as I know, Z3 is a platform that allows one to run a variety of

I'm not super informed about this but never thought of Z3 and Coq as even being related. As far as I know, Z3 is a platform that allows one to run a variety of proving algorithms, from SAT solvers to whatever. Basically, it's function is "doing things for you". Coq is called an "automated theorem prover" but really it's a platform to allow broad mathematical theories to be stated and their proofs verified. It's function isn't doing things for you, it's function is "showing you did things". But I guess, it seems, Coq has facilities like Z3. So you can translate a Z3 tutorial into Coq. Feel free to correct my ignorance here.

philzook 6y ago
Coq is usually called an interactive theorem prover, not an automated prover. Interactive provers tend to accumulate varying degrees of automation. Coq is a project at the scale of other niche programming languages. It is more of a platform than Z3 is. Z3 is more of a solver than a platform. Coq has many, many moving parts. At it's core it has a dependently typed functional programming language and specification language called Gallina. But around that is built something called the tactic system, which slightly or signifcantly automates proof steps. On top of that there are scripting system like Ltac or plugins for specialized solvers. Coq also basically requires IDE support of sorts, as the proving process is a kind of REPL converation with the system. Coq is vastly more expressive than Z3, so it makes sense that anything expressible in Z3 is expressible in Coq. What may be more surprising to people who have taken introductory tutorials is that there is significant automation in Coq, it just takes more effort and expertise than Z3's. In principle Coq could use Z3 as a plugin https://smtcoq.github.io/ https://smtcoq.github.io/ but the other direction would make no sense at the moment. Z3 is the better choice for large scale but conceptually simple queries or proofs, such as a theorem just involving linear inequalities, arrays, Ands, and Ors, or for solving constraint problems. Coq is the better choice for almost anything more complex than that.
- philzook 6y ago
  I do agree that they are usually not mentioned as competitors. Z3 does indeed basically find things, and Coq does mostly just verify things and not find them for you.
- deleted 6y ago
  [deleted]

philzook 6y ago

Coq is usually called an interactive theorem prover, not an automated prover. Interactive provers tend to accumulate varying degrees of automation. Coq is a project at the scale of other niche programming languages. It is more of a platform than Z3 is. Z3 is more of a solver than a platform. Coq has many, many moving parts. At it's core it has a dependently typed functional programming language and specification language called Gallina. But around that is built something called the tactic system, which slightly or signifcantly automates proof steps. On top of that there are scripting system like Ltac or plugins for specialized solvers. Coq also basically requires IDE support of sorts, as the proving process is a kind of REPL converation with the system. Coq is vastly more expressive than Z3, so it makes sense that anything expressible in Z3 is expressible in Coq. What may be more surprising to people who have taken introductory tutorials is that there is significant automation in Coq, it just takes more effort and expertise than Z3's. In principle Coq could use Z3 as a plugin https://smtcoq.github.io/ https://smtcoq.github.io/ but the other direction would make no sense at the moment. Z3 is the better choice for large scale but conceptually simple queries or proofs, such as a theorem just involving linear inequalities, arrays, Ands, and Ors, or for solving constraint problems. Coq is the better choice for almost anything more complex than that.

philzook 6y ago
I do agree that they are usually not mentioned as competitors. Z3 does indeed basically find things, and Coq does mostly just verify things and not find them for you.
deleted 6y ago
[deleted]