4 ms·
I think the next frontier is things like Rust. I've griped about Rust in the past but I do think that the borrow checker often feels like I'm coding in the futu
by johnfn 6y ago
I think the next frontier is things like Rust. I've griped about Rust in the past but I do think that the borrow checker often feels like I'm coding in the future - it understands my code on a much deeper level than any other statically typed language I've used.
I definitely agree with your feelings around array indices. I feel the same nervousness every time I do a slice or count backwards from the end of an array. I'm not really sure what the fix would be here, until I can just tell the computer what I want it to do, though...
- RivieraKid 6y agoBut the advantage of that doesn't apply in garbage collected languages, right?
- johnfn 6y agoActually, I wouldn't say so. e.g. Rust verifies that only one copy of my data is mutable at any one time. This is actually the kind of thing you'd always want to verify, even with a GC, because having two (say) classes that could mutate the same data instance could become a huge mess. e.g. even in GC'd languages there are libraries to provide immutable data structures because we understand that having multiple writers to data is a mess. The true ideal (for coding ergonomics) is exactly 1 writer, but there was no way to statically verify that.
- saagarjha 6y agoYou'd like to verify this always, but the Rust compiler is limited in that it can only verify this at compile time with proper annotations. As such, it rejects some valid programs.
- saurik 6y agoThat there will exist valid programs which will be rejected is true of all type systems, and that you need "proper annotations" is true of almost all type systems (and if this was worded only slightly more broadly, to discuss "proper structure" or something, it would again be true of all type systems); this shouldn't be considered a theoretical problem unless it accepts invalid programs (though it might be considered a practical problem if it is nearly impossible to correctly structure/annotate a program to make it accepted).
- saagarjha 6y ago> this shouldn't be considered a problem unless it accepts invalid programs I mean, a compiler that accepts no valid programs is problematic is it not? The way that the Rust compiler does its thing does not really work for a garbage collected language, and the comment that I was responding to, which was itself responding a restarting of what I just mentioned, said that you'd want Rust-style verification anyways for those things, which is not really an answer to the question because that kind of thing is not something that Rust can do.
- staticassertion 6y agoI think the fix is dependent types, right? If the compiler can reason about the index and the size of the vector, that's one way. For example; let x = 5; let y = vec![0; y * 2]; for i in 0..x * 3 { y[x] } That shouldn't compile.
- Kinrany 6y agoTypo: should be `[0; x * 2]`
- staticassertion 6y agoYeah, I caught it too late to edit :\
- zelly 6y agoDependent typing can make guarantees like that if there are no loops, no parallel mutation, no I/O, no cosmic rays. For example if I made y have rand() elements then there's nothing a compiler can ever do about that. In other cases the compiler can check types by executing code (not always decidable). Dependently typed languages are not Turing complete. They can help with proofs and such but it's physically impossible to use dependent types for general purpose programming (e.g. try writing Linux in Idris, you can't).
- sfvisser 6y agoDependent types strictly just means being able to parametrize types with values. You can design many different types of PLs with this feature. You don’t need strict reasoning for it to be useful like any other type level feature.
- anchpop 6y agoDependent types are cool, but I think the best fix would be refinement types. They are sort of similar, except refinement types use a SAT solver to prove correctness, while dependent types require to prove everything yourself (to the point where realistically something like what you posted probably wouldn't compile in most dependently typed languages). Refinement types also compose better. Because of the SAT solver you have some restrictions on what you can prove, but they're so much more ergonomic I think it's more than worth it.
- hardwaregeek 6y agoYeah I've been writing a lot of Rust for my compiler and it's so much fun. But it still bugs me that indexing panics. Returning an Option would make a lot more sense... What I've been wondering for my own language is whether I could design something like Rust's borrow checker but for ranges of values. That way I can guarantee valid indexing.
- swsieber 6y agoVec does provide non panicking retrieval methods. You could newtype it and implement the indexing trait, delegating to the non-panicking methods.