4 ms·

Kind of. But your conclusion is also kind of backwards: code is full of errors because it's not written very mathematically. It usually has side effects. Also,

by injb 3y ago

Kind of. But your conclusion is also kind of backwards: code is full of errors because it's not written very mathematically. It usually has side effects. Also, mathematicians are trained to think very carefully about the types of objects, and about domains and images of functions (i.e. the set of possible inputs and outputs) whereas programmers tend to leave gaps and think only loosely about these things. For example you write a function that is declared to take an integer, but then the implementation divides something by that integer. Now it can't be zero, but where do you capture that fact? Or a function is supposed to return a number but it can also return null, which isn't a number. When you tell a mathematician "this function takes an integer" or "that function always returns a string" they will immediately jump to looking for counterexamples to see if they can break it. They do this because they know that one counterexample breaks a proof. Programmers who think that way tend to produce fewer bugs imo.

amichail 3y ago
Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done.
- injb 3y ago
  >> Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done. I don't think that's it. As a rule, the tests we write for code don't prove anything in the mathematical sense. They are more along the lines of "OK it didn't break with an input of 6 or 7, now let's try 8". IOW we treat the code like a black box and see how it responds to various inputs. Mathematical proof is a different kind of intellectual activity. It's about showing that one fact is a logical consequence of another. You don't test a proof because the proof is the outcome of testing. But that testing is almost always as general as possible. In code, you might test that a given function works with the numbers 1-100 by trying 1 and 100 and simply assuming that it'll behave the same way for the numbers in the middle. This is often adequate, and it's probably the best you can do anyway, but it's not a proof (except for those specific inputs). A mathematician would instead analyze the implementation of the function to show that it's logically guaranteed to work for 1 <= x <= 100. But then the proof would only exist in their head, or on paper, in human readable form. Can you write automated tests that analyze code in that way? Maybe but that's beyond me.
  - turboponyy 3y ago
    Quickcheck is a Haskell testing library which allows the programmer to write propositions about how a function should behave, and the library will try to find cases which falsify the proposition. If my understanding is correct, it can't "prove" any properties, only disprove them. For concretely proving properties of a program, you would need something like Idris's dependent type system, where you can prove that a function always returns a sorted list, for example. https://github.com/nick8325/quickcheck https://github.com/nick8325/quickcheck https://www.idris-lang.org/ https://www.idris-lang.org/
    - tome 3y ago
      > If my understanding is correct, it can't "prove" any properties, only disprove them. Almost. If your generators exhaust the input space then the property is proved.
  - kazinator 3y ago
    "It didn't break with inputs 6 and 7" cannot be ruled out as a non-mathematical statement. Testing can be combined with inductive reasoning to validate code. Say we have some recursive function with 7 base cases, and a recursive case. We can use testing to validate the 7 base cases, and then an inductive argument that the recursive case is correct.
    - injb 3y ago
      Yes you're right. But then you're doing that by analyzing the implementation, not treating it as a black box. Personally I think we (software developers) should do more of that - i.e. take implementation details into account when designing tests, instead of treating components as black boxes, and when we change those implementation details, examine the tests to see what assumptions were made that now need to change. It's harder but it's closer to really proving something general about the code.
      - kazinator 3y ago
        That's where TDD falls down, iin fact. In TDD you first write a black-box test which fails, and then make it pass by fiddling with the interior of the white box. So, good, you then have a nice white-box test. The problem is with the refactoring step. Refactoring keeps the tests working, but some of them turn into blackbox tests which no longer relate to the internals. Like say you develop a function by adding cases, TDD style. Then you see there is a generality there and refactor so the individual cases go away. The tests probing those cases still have validity, but no value.
- kazinator 3y ago
  The person with the highest IQ in the bunch will refuse to write code when no testing is to be done.

by injb 3y ago

amichail 3y ago

Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done.

injb 3y ago
>> Maybe you need a higher IQ to write math proofs than program because you can't easily test proofs like with code? I suspect that people with higher IQ can probably write code with fewer errors when no testing is done. I don't think that's it. As a rule, the tests we write for code don't prove anything in the mathematical sense. They are more along the lines of "OK it didn't break with an input of 6 or 7, now let's try 8". IOW we treat the code like a black box and see how it responds to various inputs. Mathematical proof is a different kind of intellectual activity. It's about showing that one fact is a logical consequence of another. You don't test a proof because the proof is the outcome of testing. But that testing is almost always as general as possible. In code, you might test that a given function works with the numbers 1-100 by trying 1 and 100 and simply assuming that it'll behave the same way for the numbers in the middle. This is often adequate, and it's probably the best you can do anyway, but it's not a proof (except for those specific inputs). A mathematician would instead analyze the implementation of the function to show that it's logically guaranteed to work for 1 <= x <= 100. But then the proof would only exist in their head, or on paper, in human readable form. Can you write automated tests that analyze code in that way? Maybe but that's beyond me.
- turboponyy 3y ago
  Quickcheck is a Haskell testing library which allows the programmer to write propositions about how a function should behave, and the library will try to find cases which falsify the proposition. If my understanding is correct, it can't "prove" any properties, only disprove them. For concretely proving properties of a program, you would need something like Idris's dependent type system, where you can prove that a function always returns a sorted list, for example. https://github.com/nick8325/quickcheck https://github.com/nick8325/quickcheck https://www.idris-lang.org/ https://www.idris-lang.org/
  - tome 3y ago
    > If my understanding is correct, it can't "prove" any properties, only disprove them. Almost. If your generators exhaust the input space then the property is proved.
- kazinator 3y ago
  "It didn't break with inputs 6 and 7" cannot be ruled out as a non-mathematical statement. Testing can be combined with inductive reasoning to validate code. Say we have some recursive function with 7 base cases, and a recursive case. We can use testing to validate the 7 base cases, and then an inductive argument that the recursive case is correct.
  - injb 3y ago
    Yes you're right. But then you're doing that by analyzing the implementation, not treating it as a black box. Personally I think we (software developers) should do more of that - i.e. take implementation details into account when designing tests, instead of treating components as black boxes, and when we change those implementation details, examine the tests to see what assumptions were made that now need to change. It's harder but it's closer to really proving something general about the code.
    - kazinator 3y ago
      That's where TDD falls down, iin fact. In TDD you first write a black-box test which fails, and then make it pass by fiddling with the interior of the white box. So, good, you then have a nice white-box test. The problem is with the refactoring step. Refactoring keeps the tests working, but some of them turn into blackbox tests which no longer relate to the internals. Like say you develop a function by adding cases, TDD style. Then you see there is a generality there and refactor so the individual cases go away. The tests probing those cases still have validity, but no value.
kazinator 3y ago
The person with the highest IQ in the bunch will refuse to write code when no testing is to be done.