3 ms·

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

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.

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.