3 ms·

I am only arguing the fact that unit tests are unneeded FOR correctness now and in the future if you have the right programming methodology. If you want to wri

I am only arguing the fact that unit tests are unneeded FOR correctness now and in the future if you have the right programming methodology. If you want to write unit tests for documentation that's a different argument. I'm not against that.

alkonaut 7y ago
While a lot of domain knowledge might be possible to encode using types, most domain knowledge is probably easier to ensure via a combination of types and unit tests. It not only needs to be possible for unit tests to b me unneeded, it needs to be practical (as in economical, possible on the language used). You can probably make a formally verified first person shooter which validates the logic of its physics/network/game logic in Agda. But you likely can’t do it in C++ and be done by the holiday season. So unit tests are probably still needed and a good idea for most situations. Unit tests famously don’t prove correctness (the absence of bugs) only the presence of bugs, so I guess it’s wrong to compare them to actual verifying actual correctness.
- crimsonalucard 7y ago
  There's another emergent phenomenon that isn't often talked about for unit tests. It's known intuitively though nobody mentions it though. Unit tests are like statistical samples of all possible test cases. So unit tests while they don't verify correctness overall they can correlate with correctness. That is why you only need a couple unit tests to correlate with. a degree of correctness with a domain that's almost infinite. The phenomenon that enables science also enables unit tests to work. That being said, there are programming methodologies of managing complexity that negate the need for unit tests. This is my main point.
  - bobm_kite9 7y ago
    I like the idea of statistical samples. this makes a lot of intuitive sense. However, I'm unaware of any methodology that obviates the need for unit testing. I presume you're talking about proofs, or maybe something like Idris?
    - crimsonalucard 7y ago
      No. While dependent types or something like Idris is strongest form of correctness the technology just isn't mainstream enough yet. This is not what I'm talking about. It's really too long to get into but the programming methodology I'm talking about has to do with reducing complexity of your program to the point where your intuition along with the type checker should render unit tests mostly redundant. For example a language with no nulls renders all unit tests that test for null runtime errors unnecessary. Add exhaustive pattern matching into the mix and you'll render All tests that cover runtime errors unnecessary because your program simply can't have a single runtime error (see elm.) Both of the examples above involve either the language itself or a programming methodology or both. Rust and Haskell are two languages that force a lot of "methodology" onto your programming where a significant amount of unit tests that you would otherwise need in say python or C++ are rendered unnecessary. Another way to look at it is using a highly restrictive form of programming. The more restrictive the less opportunity for errors to the point where your intuition and type checker alone should be able to allow you to forego unit tests. There's more too it like segregating all IO from core logic but I've already written too much. Suffice to say what I'm talking about falls within a subset of the domain of a semi-popular style of programming. I don't bring up the name because that will only detract me from the main point.
      - alkonaut 7y ago
        I agree that you can remove a lot of simple representation bugs. You must have either a credit card or a billing address or your order simply cannot be in the completed state, and so on. Everything including nulls, index-out-of-bounds is unnecessary and can be elegantly handled by the type system. But complex business logic like building fire codes, tax law, network standards, traffic rules etc aren't that simple. You are quickly into Agda/Idris non-mainstream territory if you want to represent some tax law in types. It's basically "if you have two or more dependents and make under 10k then the tax is 4.5% of the income over 5k minus...". It's of course possible to represent anything using a complex enough set of types - but I haven't seen a good example of a complex piece of domain logic that didn't need tests. I'm a big fan of e.g. "Domain modeling made functional" and similar, but usually the most complex calcultions are just that: calculations. You can encode things like "the input must be positive" or "the output is guaranteed to be positive" with types easily, but when you want to encode that "given the input 3 the output must be 16 on a thursday" your are beginning to probably see diminishing returns if doing it with types instead of e.g. property based testing.

alkonaut 7y ago

While a lot of domain knowledge might be possible to encode using types, most domain knowledge is probably easier to ensure via a combination of types and unit tests. It not only needs to be possible for unit tests to b me unneeded, it needs to be practical (as in economical, possible on the language used). You can probably make a formally verified first person shooter which validates the logic of its physics/network/game logic in Agda. But you likely can’t do it in C++ and be done by the holiday season. So unit tests are probably still needed and a good idea for most situations. Unit tests famously don’t prove correctness (the absence of bugs) only the presence of bugs, so I guess it’s wrong to compare them to actual verifying actual correctness.

crimsonalucard 7y ago
There's another emergent phenomenon that isn't often talked about for unit tests. It's known intuitively though nobody mentions it though. Unit tests are like statistical samples of all possible test cases. So unit tests while they don't verify correctness overall they can correlate with correctness. That is why you only need a couple unit tests to correlate with. a degree of correctness with a domain that's almost infinite. The phenomenon that enables science also enables unit tests to work. That being said, there are programming methodologies of managing complexity that negate the need for unit tests. This is my main point.
- bobm_kite9 7y ago
  I like the idea of statistical samples. this makes a lot of intuitive sense. However, I'm unaware of any methodology that obviates the need for unit testing. I presume you're talking about proofs, or maybe something like Idris?
  - crimsonalucard 7y ago
    No. While dependent types or something like Idris is strongest form of correctness the technology just isn't mainstream enough yet. This is not what I'm talking about. It's really too long to get into but the programming methodology I'm talking about has to do with reducing complexity of your program to the point where your intuition along with the type checker should render unit tests mostly redundant. For example a language with no nulls renders all unit tests that test for null runtime errors unnecessary. Add exhaustive pattern matching into the mix and you'll render All tests that cover runtime errors unnecessary because your program simply can't have a single runtime error (see elm.) Both of the examples above involve either the language itself or a programming methodology or both. Rust and Haskell are two languages that force a lot of "methodology" onto your programming where a significant amount of unit tests that you would otherwise need in say python or C++ are rendered unnecessary. Another way to look at it is using a highly restrictive form of programming. The more restrictive the less opportunity for errors to the point where your intuition and type checker alone should be able to allow you to forego unit tests. There's more too it like segregating all IO from core logic but I've already written too much. Suffice to say what I'm talking about falls within a subset of the domain of a semi-popular style of programming. I don't bring up the name because that will only detract me from the main point.
    - alkonaut 7y ago
      I agree that you can remove a lot of simple representation bugs. You must have either a credit card or a billing address or your order simply cannot be in the completed state, and so on. Everything including nulls, index-out-of-bounds is unnecessary and can be elegantly handled by the type system. But complex business logic like building fire codes, tax law, network standards, traffic rules etc aren't that simple. You are quickly into Agda/Idris non-mainstream territory if you want to represent some tax law in types. It's basically "if you have two or more dependents and make under 10k then the tax is 4.5% of the income over 5k minus...". It's of course possible to represent anything using a complex enough set of types - but I haven't seen a good example of a complex piece of domain logic that didn't need tests. I'm a big fan of e.g. "Domain modeling made functional" and similar, but usually the most complex calcultions are just that: calculations. You can encode things like "the input must be positive" or "the output is guaranteed to be positive" with types easily, but when you want to encode that "given the input 3 the output must be 16 on a thursday" your are beginning to probably see diminishing returns if doing it with types instead of e.g. property based testing.