This. 10x.
And, if Rust's type checker could be integrated with an SMT solver to statically verify array/vector indexing (instead of performing bounds checks at runtime, or using unsafe code), that 10x would become 100x.
http://www.haskellforall.com/2015/12/compile-time-memory-saf...
However, I think this is the nuclear option. I have some experience from university where I wrote some Eiffel code, contracts and all that jazz. It often takes some head scratching to figure out the right pre- and postconditions.
I'd actually rather see more safe interfaces for the common cases (like iterators and slices) that are ergonomic to use and may actually carry the proof in their types.
(0) `pos <= str.len()`.
(1) `pos` is actually the beginning of a character - it makes sense to split the string at the position `pos`.
These things are easy to check - there is not even any multiplication involved! - but a conventional type checker won't do. Much of the pain of using dependent types is the result of sticking to unification as the only basis for type-checking.
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.
My personal experience points to opposite results of what you claim.
Let's see the hard facts rather than conjecture masquerading as such.
(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.