Eiffel contracts are still checked at runtime, which kind of defeats the point - the real payoff of enforcing an invariant statically is not having to check it dynamically! What I'm talking about is using a special kind of theorem prover called “SMT solver” to guarantee at compile time that your array indices are always valid, eliminating the need to perform bounds checking at runtime. In many cases, SMT solvers require little to no programmer-supplied annotations, which makes them more ergonomic than full-blown dependently typed programming languages like Coq, Agda, Idris, etc.
There are tools to do exactly that (I don't remember the name of what we used at university, alas). And no, I do not want to run a SMT solver against anything but simple code, because my build is slow enough as is. ;-)
Most index manipulation is fairly simple. For instance, if the result of `str.find(pat)` is `Some(pos)`, then you know that:
(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.
On the contrary, it's actually rather easy to use the type checker to encode this: Just make a wrapper type CharIdx(usize) that encodes the fact that the enclosed value is a valid char position and implement Index for it using unchecked indexing. Also implement Index for usize with the usual check for bounds and valid character position.
