5 ms·

> 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 t

> 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.

viperscape 11y ago
That's true for slicing and indexes, but hopefully you can use Iterator then for basic traversal, which does this.
- catnaroek 11y ago
  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.
  - llogiq 11y ago
    Not necessarily – you can chain iterators and skip elements on the hare.
    - catnaroek 11y ago
      You're right. I was thinking exclusively of the case where you have an array whose elements themselves are indices into the same array.
llogiq 11y ago
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.
- catnaroek 11y ago
  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.
  - llogiq 11y ago
    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. ;-)
    - catnaroek 11y ago
      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.
      - llogiq 11y ago
        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.
david_ar 11y ago
Like Liquid Haskell? http://www.haskellforall.com/2015/12/compile-time-memory-safety-using-liquid.html http://www.haskellforall.com/2015/12/compile-time-memory-saf...
- pron 11y ago
  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).
  - catnaroek 11y ago
    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.
    - pron 11y ago
      Yes, but they may also lose information in the process... As usual, it's a tradeoff.
- catnaroek 11y ago
  Yep. That was exactly what I had in mind.
pron 11y ago
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 11y ago
  > 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 11y ago
    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 11y ago
      > My personal experience points to opposite results of what you claim. Let's see the hard facts rather than conjecture masquerading as such.
    - catnaroek 11y ago
      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.

viperscape 11y ago

That's true for slicing and indexes, but hopefully you can use Iterator then for basic traversal, which does this.

catnaroek 11y ago
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.
- llogiq 11y ago
  Not necessarily – you can chain iterators and skip elements on the hare.
  - catnaroek 11y ago
    You're right. I was thinking exclusively of the case where you have an array whose elements themselves are indices into the same array.

llogiq 11y ago

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.

catnaroek 11y ago
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.
- llogiq 11y ago
  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. ;-)
  - catnaroek 11y ago
    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.
    - llogiq 11y ago
      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.

david_ar 11y ago

Like Liquid Haskell? http://www.haskellforall.com/2015/12/compile-time-memory-safety-using-liquid.html http://www.haskellforall.com/2015/12/compile-time-memory-saf...

pron 11y ago
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).
- catnaroek 11y ago
  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.
  - pron 11y ago
    Yes, but they may also lose information in the process... As usual, it's a tradeoff.
catnaroek 11y ago
Yep. That was exactly what I had in mind.

pron 11y ago

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 11y ago
> 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 11y ago
  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 11y ago
    > My personal experience points to opposite results of what you claim. Let's see the hard facts rather than conjecture masquerading as such.
  - catnaroek 11y ago
    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.