3 ms·

Is/Are there projects like Coq but with a similar aim to Z3? (I.e. being embedded into other things, with an API). I'm not exactly sure what I'm looking for sin

• philzook 6y ago
  It's a question I hadn't really considered before. On first pass, as far as I know, I'd say the answer is no. It isn't clear to me what the objective of embedding Coq with a C api for example would be. The very core of Coq is about verifying proofs and not producing them and I'm not sure what the benefit of embedding it is. Having said that there are a few projects that may be something like what you're asking. First off, Coq has the SerAPI project https://github.com/ejgallego/coq-serapi https://github.com/ejgallego/coq-serapi through which external programs can talk to coq. This has been used for example to make a python OpenAi gym like interface https://github.com/princeton-vl/CoqGym https://github.com/princeton-vl/CoqGym. A different direction might be something like MetaMath Zero https://arxiv.org/abs/1910.10703 https://arxiv.org/abs/1910.10703 which is intended to be a small and fast verifier for it's language, perhaps maybe someday for embedding in applications. There is this notion of "Proof Carrying Code" which I don't really know what the current state of the art is. https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code One might want an easily embeddable trusted verifier for that purpose. I don't know.
• amir734jj 6y ago
  You should check out sasyLF. It has a eclipse plugin as well. If you are interested in learning about proof checkers it's a good starting point. My PhD advisor is it's maintainer.