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.
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.
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.
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.
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.
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.
If you want to write unit tests for documentation that's a different argument. I'm not against that.
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.
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 presume you're talking about proofs, or maybe something like Idris?
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.
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.
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.
Type checkers do not verify behavior. Unit tests verify behavior
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.
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.