4 ms·

Could the issues of rust be rectified with a better theorem proved that goes past "2 things are touching this"? I don't think I'd mind if the compiler said "you

Could the issues of rust be rectified with a better theorem proved that goes past "2 things are touching this"? I don't think I'd mind if the compiler said "your code will not work because eventually it will modify the same bytes at the same time and create an unpredictable state" but I will mind if it says "your not good because you have two mutable references.

Diggsey 10y ago
Having a more powerful theorem prover is not always better: it makes it harder for the programmer to know whether a piece of code will work, and you can start getting non-local effects, where a change in one part of the code can break a (seemingly) unrelated part. However, what you're asking for is very similar to what types like `RefCell` and `RwLock` do - they effectively delay borrow-checking until runtime. Now you can have references to a `RefCell` in multiple places in the code, and they can all get mutable access to the interior, just not at the same time. Having said that, I find it interesting how rarely things like `RefCell` are needed in practice: there's almost always a better way to satisfy the borrow checker, and it usually results in much cleaner code.
- gravypod 10y ago
  > Having a more powerful theorem prover is not always better: it makes it harder for the programmer to know whether a piece of code will work, and you can start getting non-local effects, where a change in one part of the code can break a (seemingly) unrelated part. I think there are two solutions to that problem. The first is to involve HCI people in the development in the language to see how they can improve the output and communication from the theorm prover to the programmer. I imagine that, some time in the future, a very powerful therom prover will make its way into a "general" language and will bring some cool effects. The theorum prover I'd like to see will attempt to prove all of the conjectures used in the program and, when not possible, will say "possibly invalid code. Please solve this conjecture" where then this would be given to a mathamatician and they have to complete the missing steps to see if it works, if not we tell the compiler this isn't going to work and it now generates errors for this. The other solution is to limit the shared state of every program using very strict segregation of all moving parts and an attempt to limit use of side-effect-causing operations. This second one is nothing new, I mean the original LISP crowd had these ideas down and theres nothing new. I don't think I've ever worked with a compiler that has a built in theorum prover, possibly a shared library of proven work, and a way to in the language aid the prover. For instance this type of function definition int(int numerator, int denominator) where (denominator != 0) divide { return numerator / denominator } And even more so I've not heard of unobtrusive theorum provers that keep out of the programmers way while still being useful. I think an unproven relation should be a warning. It's not good but the program can still run and you (you being not me but the math-people) can come up after me and prove all of my work or tell me I'm an idiot and to fix it.
  - junke 10y ago
    This example works in SBCL, where types (possible disjoint sets of values) are treated as assertions. By default I always set "safety" and "debug" to 3 (the max), which helps. ;; Giving names to abstract things a little (deftype zero () `(eql 0)) (deftype non-zero () `(and number (not zero))) ;; Declaration (declaim (ftype (function (number non-zero) number) divide)) ;; Definition (defun divide (n d) (/ n d)) ;; Test (lambda (u v) ;; introduce a type constraint here. (declare (type zero v)) (divide u v)) ;; (nb: underlined in orange) This message is also printed: note: deleting unreachable code warning: Derived type of V is (VALUES (INTEGER 0 0) &OPTIONAL), conflicting with its asserted type (OR (AND NUMBER (NOT INTEGER)) (INTEGER * -1) (INTEGER 1)). See also: SBCL Manual, Handling of Types [:node] The warning happens when two types are and-ed (intersection), and the resulting set is empty. You still allow code where there is potentially "bad" value flowing from one place to another, because ultimately you know the runtime will detect it. In other words, the goal is to reject false negatives (unwarranted warnings), which contrasts with statically typed languages where you only accept code that is guaranteed to satisfy static typing rules (it makes sense there because the compiler is your last chance of catching those type errors, since the runtime does generally not perform type checks). (edit: actually use non-zero instead of (not zero))
    - gravypod 10y ago
      Yes that is exactly what I'd like but I'd like something that's grown past just type checking. There are many more bugs that I know can be caught by a theorem prover. Edit: I want to clarify. I think just type checking should be written as "Just type checking".
      - junke 10y ago
        As a matter of fact, I agree.
      - AstralStorm 10y ago
        Indeed, something like what is being tried in Pyret to make contracts (a kind of theorem lemma) the first class citizen.
lmm 10y ago
Well Rust's way of ensuring you don't modify the same bytes at the same time is to ensure that any byte has precisely one "owner" in any region in which it is mutated. That's a model we know how to implement and also an easy model for humans to think about - we can see what's going on (we can see the regions in the code) and we know what to expect to work (e.g. if you have a mutable reference you expect to be able to use it to mutate what it refers to). If you can formalize a better model you can probably implement it in a language, but what model would that be?
- gravypod 10y ago
  From an implementation standpoint that makes sense. 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". > If you can formalize a better model you can probably implement it in a language, but what model would that be? 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.
  - 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"?

Diggsey 10y ago

Having a more powerful theorem prover is not always better: it makes it harder for the programmer to know whether a piece of code will work, and you can start getting non-local effects, where a change in one part of the code can break a (seemingly) unrelated part. However, what you're asking for is very similar to what types like `RefCell` and `RwLock` do - they effectively delay borrow-checking until runtime. Now you can have references to a `RefCell` in multiple places in the code, and they can all get mutable access to the interior, just not at the same time. Having said that, I find it interesting how rarely things like `RefCell` are needed in practice: there's almost always a better way to satisfy the borrow checker, and it usually results in much cleaner code.

gravypod 10y ago
> Having a more powerful theorem prover is not always better: it makes it harder for the programmer to know whether a piece of code will work, and you can start getting non-local effects, where a change in one part of the code can break a (seemingly) unrelated part. I think there are two solutions to that problem. The first is to involve HCI people in the development in the language to see how they can improve the output and communication from the theorm prover to the programmer. I imagine that, some time in the future, a very powerful therom prover will make its way into a "general" language and will bring some cool effects. The theorum prover I'd like to see will attempt to prove all of the conjectures used in the program and, when not possible, will say "possibly invalid code. Please solve this conjecture" where then this would be given to a mathamatician and they have to complete the missing steps to see if it works, if not we tell the compiler this isn't going to work and it now generates errors for this. The other solution is to limit the shared state of every program using very strict segregation of all moving parts and an attempt to limit use of side-effect-causing operations. This second one is nothing new, I mean the original LISP crowd had these ideas down and theres nothing new. I don't think I've ever worked with a compiler that has a built in theorum prover, possibly a shared library of proven work, and a way to in the language aid the prover. For instance this type of function definition int(int numerator, int denominator) where (denominator != 0) divide { return numerator / denominator } And even more so I've not heard of unobtrusive theorum provers that keep out of the programmers way while still being useful. I think an unproven relation should be a warning. It's not good but the program can still run and you (you being not me but the math-people) can come up after me and prove all of my work or tell me I'm an idiot and to fix it.
- junke 10y ago
  This example works in SBCL, where types (possible disjoint sets of values) are treated as assertions. By default I always set "safety" and "debug" to 3 (the max), which helps. ;; Giving names to abstract things a little (deftype zero () `(eql 0)) (deftype non-zero () `(and number (not zero))) ;; Declaration (declaim (ftype (function (number non-zero) number) divide)) ;; Definition (defun divide (n d) (/ n d)) ;; Test (lambda (u v) ;; introduce a type constraint here. (declare (type zero v)) (divide u v)) ;; (nb: underlined in orange) This message is also printed: note: deleting unreachable code warning: Derived type of V is (VALUES (INTEGER 0 0) &OPTIONAL), conflicting with its asserted type (OR (AND NUMBER (NOT INTEGER)) (INTEGER * -1) (INTEGER 1)). See also: SBCL Manual, Handling of Types [:node] The warning happens when two types are and-ed (intersection), and the resulting set is empty. You still allow code where there is potentially "bad" value flowing from one place to another, because ultimately you know the runtime will detect it. In other words, the goal is to reject false negatives (unwarranted warnings), which contrasts with statically typed languages where you only accept code that is guaranteed to satisfy static typing rules (it makes sense there because the compiler is your last chance of catching those type errors, since the runtime does generally not perform type checks). (edit: actually use non-zero instead of (not zero))
  - gravypod 10y ago
    Yes that is exactly what I'd like but I'd like something that's grown past just type checking. There are many more bugs that I know can be caught by a theorem prover. Edit: I want to clarify. I think just type checking should be written as "Just type checking".
    - junke 10y ago
      As a matter of fact, I agree.
    - AstralStorm 10y ago
      Indeed, something like what is being tried in Pyret to make contracts (a kind of theorem lemma) the first class citizen.

lmm 10y ago

Well Rust's way of ensuring you don't modify the same bytes at the same time is to ensure that any byte has precisely one "owner" in any region in which it is mutated. That's a model we know how to implement and also an easy model for humans to think about - we can see what's going on (we can see the regions in the code) and we know what to expect to work (e.g. if you have a mutable reference you expect to be able to use it to mutate what it refers to). If you can formalize a better model you can probably implement it in a language, but what model would that be?

gravypod 10y ago
From an implementation standpoint that makes sense. 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". > If you can formalize a better model you can probably implement it in a language, but what model would that be? 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.
- 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"?