4 ms·

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 g

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

by Diggsey 10y ago

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.