Hacker News Reader

Comment by ChrisRackauckas | Hacker News Reader

I agree that one thing that should also be done is to change the AbstractArray interface. I believe that "being an array" and having indexing are two distinct quantities, so SimpleTraits.jl-style dispatching on "allows_linear_indexing" would be a way to slim down what's assumed when writing a function to more specific pieces (similar to Haskell). But as far as I am aware, even Haskell won't prove that a code is incorrect if it uses a hardcoded 1:n indexing in a function that says dispatches on "allows_linear_indexing" (and thus this kind of issue would get by even Haskell and not even throw a runtime error in cases where an array assumes -1:n indexing). So I'm curious, what's your idea for an interface that can prove correctness here?

View on HN

You will notice that you use the array the wrong way when you try to prove the correctness of the client of the array. Somewhere in the specification of the client it will be required to, let's say, sum up all of the elements of the array. If the array index range is [-1, 4[, but the client sums over [1, 4[, then this is wrong.

The client will have its own spec, and when it uses the array, you need to prove that it does so in a way that its own spec is fulfilled.

You need to know the entire semantics of the interaction. You need to know what the array represents for the client, and that may depend on the client of the client.

But with multiple dispatch you are constantly tempted to pretend that correctness just depends on the type, because that's what you dispatch on. So that's the problem.

In general, I like types for organising things. I don't like them for correctness.

PS: Edited the above a few times to make my point more clearly.

> If the array index range is [-1, 4[, but the client sums over [1, 4[, then this is wrong.

So you cannot loop over a subset of the indices? That seems restrictive.

You can do whatever you want. You just need to prove that it is correct. I guess I wasn't as clear as I hoped I would be.

I don't think the Array indexing issue can be dealt with by (just) improving its interface specification. I think the proper fix for this is beyond what can reasonably be done in any language that doesn't come with a notion of correctness and proof.

Dex proves indexing correctness without a full dependent type system, including loops.

See: https://github.com/google-research/dex-lang/pull/969 and https://github.com/google-research/dex-lang/blob/5cbbdc50ce0... for examples

Yes, but that doesn't handle this case. I discussed a case of indexing in the bounds which is still incorrect.

Reply on news.ycombinator.com