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
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)
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.On Monday, February 2, 2015 at 11:04:36 PM UTC-5, Brandon Barker wrote:
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
brand...@gmail.com <javascript:>
SMT-LIB (version 2) is a standard.
I think remote servers are preferred if they are practical.On Tuesday, February 3, 2015 at 3:38:56 PM UTC-5, Yannick Duchêne wrote:
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).
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.On Tue, Feb 3, 2015 at 4:38 AM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
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
.Le mardi 3 février 2015 05:04:36 UTC+1, Brandon Barker a écrit :
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
brand...@gmail.com–
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
https://groups.google.com/d/msgid/ats-lang-users/fac42f55-9349-4c0b-a93d-361d7d9f9c52%40googlegroups.com?utm_medium=email&utm_source=footer
.
Brandon Barker
brandon...@gmail.com
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.On Tue, Feb 3, 2015 at 3:56 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
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).–
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
https://groups.google.com/d/msgid/ats-lang-users/b4972bc1-9220-4214-b095-499e6be8dd83%40googlegroups.com?utm_medium=email&utm_source=footer
.
Brandon Barker
brandon...@gmail.com
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).
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).
The thread is z3 specific, but still may be worth to post a link to a list
of constraint solvers:
Solvers « Constraint Solving
But it may be biased: I noticed z3 is not listed, although it’s a famous
one.
The thread is z3 specific, but still may be worth to post a link to a list
of constraint solvers:
http://www.constraintsolving.com/solversLe mardi 3 février 2015 05:04:36 UTC+1, Brandon Barker a écrit :
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
brand...@gmail.com <javascript:>
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
.Le mardi 3 février 2015 05:04:36 UTC+1, Brandon Barker a écrit :
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
brand...@gmail.com <javascript:>