ok. i missed that. however the claim "...constraint-solver that uses machine-level arithmetic can be incorrect (but I have so far not knowingly encountered such a situation in practice)..." seems a bit too optimistic. there are and were many remote-code-execution vulnerabilities related to this. and i would like to use ats to absolutely make this impossible. (which is doable but not using the standard library)
i understand that the internal (custom) constraint solver is of limited expressiveness. would it be possible to map modular arithmetic onto SMT+QF_BV (quantifier free bitvector-arithmetic)? z3, boolector and many others have support for this. ideally an external solver could be avoided. is it possible to teach QF_BV to the internal solver in finite time and effort? http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV example: fun {m,n:bv32} bvadd ( a:bv32(m), b:bv32(n) ) : bv32(bvadd(m,n)) anyway, thanks for the great work on ats. especially the template system is something not seen in other languages. (however reminding me a bit of lisp's dynamic-bind) On Thu, Jan 4, 2018 at 7:55 PM, gmhwxi <[email protected]> wrote: > > The technique for addressing integer overflow in a general setting > seems too costly. ATS is already very complex at this point. > > The mismatch between the statics and the dynamics is explicitly mentioned. > For instance, it is mentioned in the last paragraph of the following > article: > > http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/ > HTML/HTMLTOC/x2403.html > > I want re-emphasize that this mismatch is primarily for the purpose of > making ATS more accessible. One can and probably should build his or her > own > arithmetic API in ATS when using ATS for critical low-level programming. > It is even better if one > is willing to share as well. > > > > On Thursday, January 4, 2018 at 1:09:23 PM UTC-5, cmp xchg wrote: >> >> >> hmm. but why didn't you choose the technique presented in your example >> for implementing at least array access in the main library? it seems to me >> that the current situation is even worse than in plain c. at least the >> current >> design decisions should be mentioned in the tutorial/introduction >> sections? >> > -- > You received this message because you are subscribed to a topic in the > Google Groups "ats-lang-users" group. > To unsubscribe from this topic, visit https://groups.google.com/d/ > topic/ats-lang-users/PREd1G9K0Aw/unsubscribe. > To unsubscribe from this group and all its topics, send an email to > [email protected]. > To post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/ats-lang-users. > To view this discussion on the web visit https://groups.google.com/d/ > msgid/ats-lang-users/bcb8969a-29a8-4fa4-b196-1180de54ade5% > 40googlegroups.com > <https://groups.google.com/d/msgid/ats-lang-users/bcb8969a-29a8-4fa4-b196-1180de54ade5%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAKpwDv%3DuDZ5wRpu90w5hJbti-aJ8%3D0GnsoH869YUYPoZ4J%2BW0A%40mail.gmail.com.
