[nigeltao]

Re ATS, 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]

ATS 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.