A type checker should track an aspect of this thoroughly. If you find yourself relying unit tests as a contract to prevent future changes something is wrong with your coding methodology. Too many dependencies in your code, not enough modularity.

If your coding methodology was good, the type checker is enough to verify these contracts.

A language without a type checker will have more need of unit tests.

A type checker is very helpful, but type checkers catch a few different type of error from unit tests. I would not want to refactor a large program without both.

Unit tests ensure that everything you thought about still works. Types ensure that ALL types are compatible.

What types do well is the everything case, you cannot forget something with types. However they only cover compatibility not correctness. You can have a type correct program that is wrong.

There are formal methods can can get to correctness. If you have the right constraints. The only problem is you can have the wrong constraints. Within that limit though it shows the program works correctly in all cases.

Unit tests prove only the cases you thought about work. While this is far below the infinite number of cases the above prove, they are still very useful because it is generally very easy to reason about the one case you do choose. If you choose the cases well, the majority of possible cases are "close enough". Thus a few well chosen unit tests can give you assurance that your code works correctly in the important cases.

Unit tests operate in the same domain and constraints as formal methods. In terms of correctness formal methods beat unit tests hands down.

For things that live outside of this domain the term integration test becomes relevant. If you are testing for unknown side effects it is no longer a unit test but an integration test.

This is not my point.

Unfortunately I can't go into detail about my point because it's just too long to talk about. I glossed over it and called it "Programming methodology."

In the context of correctness, with the right programming methodology, programming language and type checker you can use this and your intuition alone to forego the need for unit tests. This does not apply to integration tests.

Anyway without going in to deep the right programming methodology involves reducing complexity. It's similar to how if a programming doesn't have nulls you can't have runtime errors caused my nulls. If you use the right programming language or right methodology you can reduce much of the complexity of the program to the point where unit tests are redundant to your intuition.

Another good example of a language that pulls this off is Rust or Haskell. You don't have to go as far as COQ but the previous two languages force you into a methodology that ensures correctness to a degree that many unit tests become redundant.

Formal methods don't beat unit tests for one important reason: it is much easier to reason about the single case the unit test covers and convince yourself it is correct than about all the possible cases (which might be an infinite set) at the same time. As Donald Knuth has said "Beware of bugs in the above code; I have only proved it correct, not tried it". Because even Knuth himself is smart enough to know he sometimes makes mistakes in his proofs. Just a few trials (ie unit tests) give confidence it works in practice and in theory.

Or to put it a different way, unit tests guard against an incorrect specification. Code can be proven correct and wrong at the same time. Unit tests make it much easier to reason about if what is specified to happen is what should happen.

As an aside, I'm not against blurring the line between unit tests and integration tests.

>Formal methods don't beat unit tests for one important reason: it is much easier to reason about the single case the unit test covers and convince yourself it is correct than about all the possible cases (which might be an infinite set) at the same time.

Dependent types and/or automated proof checkers should bridge the gap of intuitive reasoning. Basically the dual relationship where code verifies the type and dependent types verify the code should be strong enough to forego unit tests and guard against "incorrect specification."

>As an aside, I'm not against blurring the line between unit tests and integration tests.

Sure that's fine. But then the type of test and the context of what I am referring to is strictly tests that only cover pure mathematical logic.

Things outside of that bound cannot be covered by proof nor by programming methodology and are also not the type of test I am referring to.

A type checker still accepts a correct but enormous interface without complaint. It’s only when you want to test it in isolation you realize that the function needs a dog+kitchen+universe you have trouble providing. So you refactor it to have a smaller interface and that lets you write the test. The act of writing the test now made you write less coupled software and it will remain and prevent anyone from adding the coupling in the future.

For me this is the best side of unittests: their validation of “correctness” is just one aspect, but their job as a guarantee of decoupling and a living documentation is at least as important. Even a test that is only written and compiled but never run provides great value for architecture and documentation.

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.

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.

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.

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?

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.

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.

I get where you're going with this. You are talking about macro phenomena of multitudes of simple axioms interacting with each other.

Let me put it this way:

Given an exact set of tax laws, network standards or traffic rules I can implement this perfectly and easily with types, intuition and programming methodology alone. (Another hint: don't use mutable variables or even better forego variables and go point free; it eliminates a whole class of bugs that has to do with state.)

Implementing a specification is trivial even when the specification is complex. It's simply a mapping from english to programming logic. There is little complexity here.

I think what you're getting at is a sort of derivation of the specification from a macro goal.

For example, what is the best way to tax society so that society has maximal benefit and zero loop holes for bad actors? What is the best way to create a set of traffic rules and network standards so that throughput is maximized, fair among everyone, and (most importantly) 100% bug free?

This is hard and specs derived from a macro goal can be bad or wrong. This also usually happens before programming begins.

Bad specs are not something that unit tests are really used for. Unit tests are used for logic errors. To catch where a programmer implemented a spec incorrectly.

While I can see some logical value for using unit tests to test for macro level goals this stuff in practice happens at the IO level and is the domain of integration tests. You are not testing a "unit" when measuring a macro level goal, the philosophy of an integration test applies in this case because a macro level goal is basically operating at the integration level rather than the unit level.

crimsonalucard's reply is a good summary, but it must be understood that this kind of thing obviates the need for some unit tests, not all unit tests. Haskellers love unit testing, after all! (See QuickCheck and HedgehogQA).

For very simple programs, sure.

Type checkers do not verify behavior. Unit tests verify behavior

Unit tests do not verify behavior, except for a few cases (out of a virtually infinite set of cases) that the programmer happened to think about.

Types do verify behavior - e.g. this function always returns an Int, that function only returns a UserId, this other function doesn't do any I/O.

That is a very different behavior though. If my multiply function returns ADDs the input and returns an int it passes the type checker but is still wrong.

But if your multiply function fails to handle some special case that the tests don't catch (negatives, overflow/saturation, denorms, ...) then the tests are also wrong.

What you really want is to be able to state properties, e.g. "for all x/y, mul(x, 0) = 0, mul(x, 1) = x, mul(x, 2) = x + x, mul(x, y) = mul(y, x)", and so on. And working with these kinds of statements (via e.g. quickcheck or whatever) might generate tests, but feels a lot more like working with types. You're making proofs, not examples.

Which is why I have always (well for the last 5 years or so anyway) said that you want both because they catch different issues.