It is! And I'm a big fan of test systems that optionally invert the logic and require failure - to weed out bullshit tests.
But there are some things that are challenging to test for. Tests sample the space, proofs define the space. you can't build it wrong. (you can sure have a bad spec, and build the wrong thing though)
Tests definitely help. It sorta feels like there's value left on the table. The spec, the types let you define broader constraints, and you catch them all.
I'm one of the people who believe that TDD and safety-by-design (which is based on strong, static typing) are actually two sides of the same coin. In a sufficiently powerful type system, they could possibly even be two implementations of the same thing.
- Start with spec.
- Write the specs as something that the compiler/test harness will check for you.
- Write the code.
The main differences being, of course, that you'll typically get your compiler error messages much faster than your test error messages (typically while you're writing the code), which makes them easier to fix - on the other hand, in pretty much all languages, the type system isn't expressive enough to represent all the specs that can be represented as tests.
In other words, in the current state of the world, we need both.
They're attacking the problem from two directions - bottom up and top down.
I view the type system as a way to whittle down the state space to the bare minimum while the tests validate that that the behavior of that whittled down execution space matches what is required.
I think investment in a type system to replace tests very quickly reaches a point of diminishing returns and vice versa. A really good type system won't ever beat ok tests + an ok type system and vice versa.
But there are some things that are challenging to test for. Tests sample the space, proofs define the space. you can't build it wrong. (you can sure have a bad spec, and build the wrong thing though)
Tests definitely help. It sorta feels like there's value left on the table. The spec, the types let you define broader constraints, and you catch them all.