> It may be harder to write Rust code than Java code, but it’s a lot harder to write incorrect Rust code than incorrect Java code.
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.
Well, yes and no. You can prove all the properties liquid types can without actually using liquid types, just by running the algorithms that infer them. Either way (inferring with or without types) the problem of indexing is undecidable, and cannot be verified in the general case (but it can in many common usages).
The point to using types is that they make static analyses more compositional. Types enforce invariants across module boundaries, without requiring the entire program to be checked in a single pass.
I'd personally like to find the time to write this – some of the infrastructure (like call graph analysis) is already available.
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.
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.
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.
Yep, when iterators do the trick, they're preferable to indexing. But some algorithms (e.g., the tortoise and hare algorithm for cycle detection) explicitly require indexing.
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.