4 ms·

I agree! I see a lot of stuff like "static typing is better than tests", "tests don't prove your code is bug free" etc as if tests somehow have to be a silver b

I agree! I see a lot of stuff like "static typing is better than tests", "tests don't prove your code is bug free" etc as if tests somehow have to be a silver bullet to justify their existence. I definitely think its ok for the overall standard of test code to be lower than production code though (I guess horrible unmaintanable tests is maybe a bit much). A few reasons I can think of off the top of my head: - You can easily delete and rewrite individual tests without any risk - You don't ship your tests, bugs and errors in tests suites have a way smaller chance of causing downstream issues for customers (not the same as no chance but definitely a lot smaller) - I'd rather have a messy, hard to understand test than no test at all in most cases. That isn't true of production code at all, there are features that if they can't be produced in a coherent way with the rest of the codebase just don't have the value add to justify the maintenance burden.

gorgoiler 3y ago
I often think of unit tests as being programmable types, like Eiffel pre/post conditions or functional languages with types like Even and Odd. For example, in double(x) -> y you can use types to say x belongs to the set of all integers and y must also must be in that set, but that’s about all you can say in Python. Unit testing lets you express that y must be an even number with the same sign as x. It is like formal verification for the great unwashed, myself included.
- feoren 3y ago
  But you literally cannot possibly test that assertion for all x. Let's take a slightly harder problem: prove (or at least test conclusively) that for all integer x, the output y of the following function is always even: y = x^2 + x + 2 There is essentially no way to prove this for all x by simply testing all integers. If your integers are 64-bit, you don't have enough time in the lifespan of the universe. On the other hand, you could simply reason through the cases: if x is even, then all terms are even. If x is odd, then x^2 is also odd, and x^2 + x = odd + odd = even. So you're done. This is what people mean when they say "tests don't prove your code is correct" -- it's almost always better to be able to read code and prove (to some degree) that it's correct. It's really nothing like static types, which are also constructive proofs that your code is not incorrect in specific ways. (That is: it proves that your code is not [incorrect in specific ways], not that your code is [not incorrect].) Once you prove your code correct, you can often write efficient tests with cases at the correct boundary points to make sure that proof stays correct as the code changes.
  - randomdata 3y ago
    > But you literally cannot possibly test that assertion for all x. Hence why he states it is formal verification for the "unwashed masses". The "washed" will use a language with a type system that is advanced enough to express a formal proof, but most people can't hack it, and thus use languages with incomplete type systems and use testing to try and fill in the gaps.
  - gorgoiler 3y ago
    Could you do this in Python (using positive integers as an example of a type rather than even numbers)?: class N(int): def __init__(self, z: int): assert z > 0 super().__init__(z) def log2(n: N) -> float: … log2(N(32)) # 5.0 log2(32) # type error log2(N(-32)) # runtime error You are still relying on the runtime to detect errors and it’s annoying to have to cast all ints to Ns, but you at least won’t ever take the log of a negative number.
    - benrutter 3y ago
      That's a cool trick! Depending on your use case though it might not go far enough since the new "type" is really just an integer with an assert. It won't be picked up by static type checkers and there's nothing stopping you doing this: ``` x = N(2) x -= 10 ``` I think x still winds up being less than 0 here? Its probably easier just to add an "assert" with a friendly message at the start of the log function.

gorgoiler 3y ago

I often think of unit tests as being programmable types, like Eiffel pre/post conditions or functional languages with types like Even and Odd. For example, in double(x) -> y you can use types to say x belongs to the set of all integers and y must also must be in that set, but that’s about all you can say in Python. Unit testing lets you express that y must be an even number with the same sign as x. It is like formal verification for the great unwashed, myself included.

feoren 3y ago
But you literally cannot possibly test that assertion for all x. Let's take a slightly harder problem: prove (or at least test conclusively) that for all integer x, the output y of the following function is always even: y = x^2 + x + 2 There is essentially no way to prove this for all x by simply testing all integers. If your integers are 64-bit, you don't have enough time in the lifespan of the universe. On the other hand, you could simply reason through the cases: if x is even, then all terms are even. If x is odd, then x^2 is also odd, and x^2 + x = odd + odd = even. So you're done. This is what people mean when they say "tests don't prove your code is correct" -- it's almost always better to be able to read code and prove (to some degree) that it's correct. It's really nothing like static types, which are also constructive proofs that your code is not incorrect in specific ways. (That is: it proves that your code is not [incorrect in specific ways], not that your code is [not incorrect].) Once you prove your code correct, you can often write efficient tests with cases at the correct boundary points to make sure that proof stays correct as the code changes.
- randomdata 3y ago
  > But you literally cannot possibly test that assertion for all x. Hence why he states it is formal verification for the "unwashed masses". The "washed" will use a language with a type system that is advanced enough to express a formal proof, but most people can't hack it, and thus use languages with incomplete type systems and use testing to try and fill in the gaps.
- gorgoiler 3y ago
  Could you do this in Python (using positive integers as an example of a type rather than even numbers)?: class N(int): def __init__(self, z: int): assert z > 0 super().__init__(z) def log2(n: N) -> float: … log2(N(32)) # 5.0 log2(32) # type error log2(N(-32)) # runtime error You are still relying on the runtime to detect errors and it’s annoying to have to cast all ints to Ns, but you at least won’t ever take the log of a negative number.
  - benrutter 3y ago
    That's a cool trick! Depending on your use case though it might not go far enough since the new "type" is really just an integer with an assert. It won't be picked up by static type checkers and there's nothing stopping you doing this: ``` x = N(2) x -= 10 ``` I think x still winds up being less than 0 here? Its probably easier just to add an "assert" with a friendly message at the start of the log function.