4 ms·

From an implementation standpoint that makes sense. From a usability standpoint it does not. The use case of systems programming usually involves many mutators

• lmm 10y ago
  > From a usability standpoint it does not. The use case of systems programming usually involves many mutators on a single piece of, non-copiable, data. I can see why the person writing the Rust prover would say "yea this is the best" but I can't see why anyone else would because it's filter cuts out a large portion of completely valid code that is not incorrect but instead is "scary" or "spooky". I find passing ownership around very usable, and can never understand how the bit-twiddling C folks ever get anything done. Maybe that's my mathematical background - I like my functions to be functions. > I'm just someone on the internet here to complain. I can't do that because I'm not a smart math person who can prove how to get there or even generalize it to work with other programming related things. The hard part is forming the model. Once you actually know how it's supposed to work, proving it is the easy part. But I mean, how would you even explain to another human that a given algorithm is safe, if not by arguments along the line of "look, this function owns this piece of data and this function owns this piece of data and they're called one after the other"?
  • gravypod 10y ago
    > The hard part is forming the model. Once you actually know how it's supposed to work, proving it is the easy part. But I mean, how would you even explain to another human that a given algorithm is safe, if not by arguments along the line of "look, this function owns this piece of data and this function owns this piece of data and they're called one after the other"? One example of how this could work is writing a spinlock. Let's use a made up language for now and adapt that to our need. alias lock unsigned int; lock() make_lock ( return 0; ) void(ref<lock> l) take_lock ( while (l != 0); // Assume this is atomic for brevity l += 1; ) void(ref<lock> l) give_lock ( l -= 1; ) This is a "correctish" non-reentrant lock. This has many vectors to see if this is "correct" from a compiler standpoint. The first is that only the alias "lock" can be passed to my lock even though it is just an "unsigned int". Another mode is that I am doing (lock -= 1). Since this is unsigned if my program ever gets into a state where I am doing (0 - 1) in unsigned arithmatic then I am going to wrap around to UInt.MAX_VALUE which is not how subtraction should behave and it should warn me when this situation arises. If the language allows me I can also do this to help the compiler know that I never want this to happen. void(ref<lock> l) where (l != 0) give_lock ( l -= 1; ) Now the compiler can see I absolutly do not want this wraparound behavior and it can check for it. Where would this be the case? int() thread_safe_fac(ref<lock> l, int some_important_data) ( int f; take_lock(l); if (some_importand_data) { f = some_important_data * thread_safe_fac(l, some_important_data - 1); } else { f = 1; give_lock(l); } give_lock(l); return f; ) void() main ( lock l = make_lock(); int some_important_data = 10; some_important_data = thread_safe_fac(&l, 10); print(some_important_data); ) Will this code work? Absolutly not and it's easily checkable. One of my function's invariants is violated. give_lock() will sometimes fall negative. This is a very crude example but I've seen code like this in larger projects where someone modified some code and someone refactored that then someone was contracted to add a feature. It just goes down the shitter. But this is easily provablely wrong. * Call thread safe fac * grab a lock * we theoretically touch some thread safe data * We hit a case where we do an if * Then run the then case * else set a default and free our lock * Free our lock We've free'd twice and we've now broken the underyling data of the `lock` type. We've got an unsigned int that has been wrapped around to an huge number and take_lock(l) will never work again. Lock is a mutable datatype that can be shared between N many threads/fucntions and it can always be checked like this just by telling the compiler "hey I never want to let the internal int fall into a state where it is subtracting 1 from 0". This can also be extended to other things void test(int *num) { *num *= 10; } int some_complex_function(int *num) {... free(num) ... } int main() { int *some_cool_data = (int*) malloc(sizeof(int); *some_cool_data = 5; while (true) { ... test(some_cool_data); ... some_complex_function(some_cool_data); ... } } We've come to a place in the code where we have a possible path of execution (regardless of the depth in if statments or gotos or other control flow) where we will eventually come to the point where we use a bit of data after it's free'd. This code will be correct if you do something like. // We now make sure the compiler knows that we only want to accept real references to initialize ptr int some_complex_function(int **num) where (num && *num) {... free(*num); *num = NULL; ... } // We've removed the path through the program that allows the data to be used after free. while (some_cool_data) { ... some_complex_function(&some_cool_data); ... } Again another bad example but there is a lot of perfectly valid, and very clean code that is against the borrow checker but is still completely correct.
    • lmm 10y ago
      I don't think I understand your point. You can use e.g. Nat in Idris to avoid the underflow possibility. A language shouldn't allow silent overflow, and to the extent that Rust encourages a style where you fiddle with overflowing integers this is a problem with Rust, though I don't believe Rust does encourage that style - it provides locks, and if you were writing a custom one for some reason you wouldn't naturally fiddle with an int, you'd use an affine type or some such.
• kazagistar 10y ago
  Lots of mutators over a single piece of data gets you data races. If you do it correctly, you protect against this somehow, using something like a mutex, or something more complex. Rust provides RefCells, Mutexes, and fancy libraries like Crossbeam for exactly this reason.