3 ms·
ATS could probably do some of this by constructing proofs about the bounds and indices - not in the completely general case of course, but for at least some fra
by zem 3mo ago
ATS could probably do some of this by constructing proofs about the bounds and indices - not in the completely general case of course, but for at least some fraction of what a language without dependent types would have to defer to runtime
- ratmice 3mo agothose are not dynamic bounds.
- LoganDark 3mo agoAll "dynamic" means is that you don't know or don't prove the precise value statically. However you may know the range of possible values, or you may know properties of your algorithm that mean it can never attempt an out-of-bounds access. Sometimes you don't know any of these things, but sometimes you do.
- ratmice 3mo agoWhat I was (badly) trying to express was more that given static bounds rust could also eliminate dynamic checks. So saying e.g. ATS can eliminate static checks, is kind of switching the target.
- zem 3mo agohttps://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3196.html https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML... is the kind of thing I mean - ATS programs can include proofs that an array access will be safely within bounds, even if we don't have an exact literal subscript in the code.