On: Comparing Rust and Java

[pron]

The problem of array overflow/underflow is undecidable in the general case. Various verification techniques (like SMT solvers) can only prove some usages, but not all.

[catnaroek → pron]

> The problem of array overflow/underflow is undecidable in the general case.

Obviously.

> Various verification techniques (like SMT solvers) can only prove some usages, but not all.

Turns out this is good enough for most cases. Verifying 80% of your array index manipulations is better than verifying none of it.

[armitron → catnaroek]

Where do you get "good enough for most cases" or the 80% from? Let's see the hard facts rather than conjecture masquerading as such.

My personal experience points to opposite results of what you claim.

[ant6n → armitron]

> My personal experience points to opposite results of what you claim.

Let's see the hard facts rather than conjecture masquerading as such.

[catnaroek → armitron]

My main use cases for manipulating indices directly are:

(0) Implementing lexical contexts and environments whose variables are identified with de Bruijn indices or levels.

(1) Implementing multidimensional arrays and operations on them (e.g., matrix multiplication).

In both of these cases, a solver for the theory of integer arithmetic can check that I'm using my indices right.