z3 constraint solver

[Brandon Barker]

What will be the practical differences (i.e. introduced features) of using z3, or is it just about efficiency?

I hope the answer is that more constraints can be handled :). Smarter solver allows for dumber programmer, maybe...

--

Brandon Barker
brandon...@gmail.com

[Yannick Duchêne]

There is the license to watch carefully too, and the commercial license is far too expensive for a standalone developer: $9,999.00. That's not a joke, that's really the price: http://www.microsoftstore.com/store/msusa/en_US/pdp/Microsoft-Research-Z3-Theorem-Prover/productID.279030500 .

[Yannick Duchêne]

The thread is z3 specific, but still may be worth to post a link to a list of constraint solvers:

http://www.constraintsolving.com/solvers

Le mardi 3 février 2015 05:04:36 UTC+1, Brandon Barker a écrit :

[Yannick Duchêne]

Le mardi 3 février 2015 15:12:05 UTC+1, Yannick Duchêne a écrit :

The thread is z3 specific, but still may be worth to post a link to a list of constraint solvers:

http://www.constraintsolving.com/solvers

But it may be biased: I noticed z3 is not listed, although it's a famous one. 

[Brandon Barker]

Wow. At that price, they at least want you to think it is good :).

I wish I knew more of the field; I think I need to find a way to gain perspective for theorem-proving in programming. You mentioned last year you didn't like some things about Coq, other than it not being a real language. I'm curious what you didn't like about it. It seems lots of people are using Coq; granted these are probably mostly mathematicians who did a PhD in type theory or homological algebra, which I am not. 

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/fac42f55-9349-4c0b-a93d-361d7d9f9c52%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[gmhwxi]

Efficiency is less of a concern right now.

Z3 can handle constraints from domains other than the domain of integers.

In general, it would be good to move constraint-solving out of ATS2. Maybe
we could have a server in the future for solving constraints and certifying ATS
code that has passed typechecking.

[Yannick Duchêne]

Le mardi 3 février 2015 21:12:03 UTC+1, gmhwxi a écrit :

Efficiency is less of a concern right now.

Z3 can handle constraints from domains other than the domain of integers.

In general, it would be good to move constraint-solving out of ATS2. Maybe
we could have a server in the future for solving constraints and certifying ATS
code that has passed typechecking.

A local server or a remote server? Moving the constraint solver outside of ATS and expect to be able to switch from one solver to another, would require a standard protocol. I remember it was discussed last year and I suggested some pointers (but I forget the name of that standard now).

[gmhwxi]

SMT-LIB (version 2) is a standard.

I think remote servers are preferred if they are practical.

[Yannick Duchêne]

Le mardi 3 février 2015 15:36:17 UTC+1, Brandon Barker a écrit :

Wow. At that price, they at least want you to think it is good :).

I hope for their clients it is really (that's an issue in the software world in the large… it's either free, either expensive and nothing between… at least so far).

 

I wish I knew more of the field; I think I need to find a way to gain perspective for theorem-proving in programming. You mentioned last year you didn't like some things about Coq, other than it not being a real language. I'm curious what you didn't like about it. It seems lots of people are using Coq; granted these are probably mostly mathematicians who did a PhD in type theory or homological algebra, which I am not. 

Some PhD are using Isabelle too. I'm not so much against Coq and pro‑Isabelle, and more see good and bad points with both. As a summary : Coq has a logic where type as proof and Curry‑Howard isomorphism are immediately apparent, while Isabelle is less obvious with this; Isabelle has a nice and structured proof language (except for its keywords) and generate nice proof texts you can read outside the Isabelle environment, while Coq proof looks less natural and can't be read outside of the Coq UI and its display of proof's states; Coq makes use of clean and readable plain English keywords à la Ada, while Isabelle use confusing and abbreviated/cryptic keywords; Isabelle's favorite logic, HOL, is more famous and more well know than Coq's logic, CoC; Coq core system is simply an implementation of its core logic, while Isabelle first implement a meta‑logic in a system which is hard to understand really; Coq UI is more fluid and lightweight (native GTK) than Isabelle UI (jEdit and Java); Isabelle is implemented in SML (safe), while Coq is implemented in an alleged safe subset of OCaml (which is unsafe to me).

Both share some bad points: hard to generate program source outside of their native target (SML for Isabelle and OCaml for Coq); generated program sources make use of infinite precision numbers only (bignums are not efficient); both are better suited to purely mathematical proof than to programming, although they are both advertised as being able of this.

That's what comes to my mind trying to reply quickly.

By the way, I planned to have a look back at Coq in the future (just to say that I don't hate it).

[Yannick Duchêne]

Le mardi 3 février 2015 21:48:08 UTC+1, gmhwxi a écrit :

SMT-LIB (version 2) is a standard.

I think remote servers are preferred if they are practical.

Yes, SMT‑LIB, that's it. Thanks for the memory.

Remote server may be nice with constraints hard to deal with (Isabelle do this), but for simple things, why not keep things local? (Isabelle has this too… both options)

[Brandon Barker]

Thanks for the detailed reply Yannick. When listening to your analysis, I do find it very hard to choose between which to try. I will probably hold off for a bit.

Note, if you are trying to look for Isabelle and Homotopy Type Theory (HoTT), it is prudent to not google for: Isabelle HoTT. Although it seems like the HoTT community went with Coq, I can't begin to know if that was more or less a preferential decision vs a logical necessity.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b4972bc1-9220-4214-b095-499e6be8dd83%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com