3 ms·
Re ATS, http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2403.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/... says that "By def
by nigeltao 9y ago
Re ATS, http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2403.html http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/... says that "By default, the constraint-solver implemented for ATS/Postiats makes use of the standard arithmetic of infinite precision. For the sake of efficiency, one may also choose to use machine-level arithmetic for solving integer constraints. Due to potential arithmetic overflow, results returned by the constraint-solver that uses machine-level arithmetic can be incorrect".
Puffs does not use infinite precision integers (aka "big ints"), for performance. But Puffs still checks for arithmetic overflow.
Re dependent types, I made a comment elsewhere on this page that "dependent types are one way to prove bounds safety, but they're not the only way".
- doublec 9y agoATS uses infinite precision ints only for the proof/dependent type checking. The ints used at runtime are machine ints. It's to avoid overflow during type system checking.