So, how often is poorly tested code out there? From the popularity of strong static typing, it must be ubiquitous.
If a developer can jump into an unknown part of a codebase and quickly see that following a certain structure will automatically make their code work for them without needing to read all the code first and double checking if it's just a random convention versus a strict interface so they don't reinvent the wheel or build code that doesn't fit in with the existing structure, then that's worth a lot and something you cannot simply cover with tests.
It is like the things you already trust when you code. Let's say, that the file system works, that the network stack of your OS works, or that the cpu works. You can rely on them to use your time for the things that matter. This is a much better model than simply testing everything yourself since, as the tests number increase, any change to the codebase involves more and more test changes.
> Strong static typing is useful in the environment where the code is not adequately tested. That's because tests adequate to make the code bulletproof will also detect the problems strong static typing could detect, rendering SST superfluous.
Your logic is the same as follows: seat belts are useful in an environment where drivers are not driving adequately. That's because adequate drivers will drive in a way to avoid any danger that the seat belt would prevent, rendering seat belts superfluous.
Ultimately, the problem is adequate drivers (as in described above) or bulletproof tests do not exist, they are just a concept. A test can prove the presence of an error, not the lack of errors, and the argument only works in absolutes.
The analogy with driving doesn't make much sense. After all, accidents sometimes happen without the driver being to blame, and the marginal cost of putting on a seat belt is very low.
Apart from an analogy is a template of your argument. It is the logic of the argument itself.
Errors also happen sometimes without type systems being to blame (they only catch a subset of errors).
The marginal costs of a type system is usually very low too, so it seems to be a great fit.
Static verification (what includes static types) is the real deal.
That said, WTF is there with people insisting that types must be either static or dynamic, and that dynamic types are useless?
Whoever said you can only pick one of the two approaches?
If anyone can think of something a unit test could test for that an arbitrarily* complex/strong type system couldn't I'd be interested to hear it. It's possible, I just can't think of any.
An arbitrarily complex type system, with dependent types, could detect any bug, since it's formally equivalent to requiring the program be proved correct. But using such a type system is so onerous that I don't know anyone who realistically does it in production.
If you wrote such types, you're basically giving a formal specification of what the program is supposed to do. That could then be used, and likely much more easily, for high volume property-based testing.
More info here: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
if you have a type system expressive enough to do things like that, you've basically got another turing-complete layer on top of your existing language, which is itself ... dynamically typed.
Ok, but it's cheaper to not have to write those tests than it is to write those tests.
That's quite clearly not what I'm saying.
When you use a typed language, you can use your integration tests to actually verify business logic, exception handling, etc. instead of having to write a dozen test cases to make sure that doThing(table, index,*kwargs) doesn't blow up when 'table' is a list or 'index' is bytes...
(It won't find latent bugs that can't currently be exercised, so the testing can't be one and done.)
if you use a static type system you can guarantee there will be no type errors at runtime. why on earth wouldn't you choose that? you can still write logic tests!
and when you leverage the type system to make illegal states unrepresentable, you can make certain classes of logic error impossible as well. some of your tests become tautologies and you can delete them.
What testing cannot find are latent errors not exercised by the program. Do I care about these, though? Arguably these would be found by testing internal interfaces and elimination of code not reachable by tests.
The general argument I am trying to make is that the marginal value obtained by strong static typing declines as testing increases, and that in the limit goes to zero. If a program is adequately tested, is it still worth doing? This is not clear to me, and the arguments given here have not convincingly demonstrated that it is worth it.
Also: if you find yourself in a situation where strong static typing seems useful, you should be alarmed. It means you aren't testing your code very thoroughly.
I am not assuming that.
honest question: what language do you have in mind when you think "static types"? your perspective is so starkly different to mine, you seem to be operating under totally different assumptions about what types can and can't do.
I mean this sentence:
>Also: if you find yourself in a situation where strong static typing seems useful, you should be alarmed. It means you aren't testing your code very thoroughly.
is just baffling to me. it's so self-evidently absurd that I can't even argue against it. what is there even to say?
have you even used a modern statically typed language, with type inference, generics, null safety, algebraic data types, pattern matching, etc? I cannot imagine trying to maintain a big codebase without them. they don't slow me down, they speed me up. they aren't just about catching trivial int-instead-of-string bugs, they are are core tool for modelling data and business logic. they let me define problems out of existence (see e.g. this series of posts https://fsharpforfunandprofit.com/posts/designing-with-types... for an introduction).
and then there's rust and newer-generation languages with borrow checkers and affine/linear types, ruling out entire classes of memory and concurrency bugs ... your test suite cannot rule out data races, but rustc sure can.
you are making the same arguments people were making in the 2000s when most static languages sucked because they didn't have these features. I don't want to go back to a time before sum types.
>What testing cannot find are latent errors not exercised by the program. Do I care about these, though?
you should, because in production your program must endure orders of magnitude more variety in inputs, uptime, and runtime conditions than the test suite can exercise. it can and will get into weird states you didn't anticipate. yes, you can fuzz, yes you can property test, I know all about that. those things are good. but I don't get why you wouldn't also use a static type system to provably rule out classes of problem across all possible code paths. why settle for less?
Because type errors in unit tested code are basically non existent. It's a fictional problem and as such there is no point in spending real resources chasing fictional problems.
There is plenty of research that shows that static typing gives no benefits (statistically insignificant) when it comes to software correctness.
What you are asking is why shouldn't the local government spend money on a Yeti patrol to protect the general public against Yeti's? The Yeti patrol will eliminate an entire class of problem (Yeti attacks).
this is short-sighted. I am not talking about trivial string-instead-of-an-integer errors here. powerful type systems let you encode far more sophisticated constraints on the program. safe rust makes data races into a compile-time error via its type system, for example. unit tests can't do that.
I think you're greatly underestimating what types can do for you. you seem to have this mental model where you would write the exact same kind code with a type checker as without one, and the only difference is whether you have to convince some pedantic bureuacrat that your code is correct when you already know it is.
but when you have a powerful type system, you don't write the same kind of code. the type systems helps drive design, similar to how tests can drive design. you have probably seen code that is bad because it wasn't written with testing in mind. there wouldn't be much value in adding unit tests to the code right away -- you probably need to do some highly invasive re-architecting to make it testable.
so, is it really such a stretch of the imagination that code can also be deficient because it's untypeable? perhaps the reason you don't see much benefit to types is because you didn't write the code with types in mind, as a design tool.
there is a learning curve to writing testable code. the same is true for types.
read this if you haven't, about type-driven design: https://fsharpforfunandprofit.com/series/designing-with-type...
No, my mental model is removing the type checker allows me to write shorter, more concise and higher quality code. Dynamic typing enables much better code styles than static typing.
> the type systems helps drive design
Ahh you are an complexity merchant, if only I made my code more complicated all my problems would be solved. I'm afraid not, the more complicated your code the worse it is.
No I'm afraid, I have actual real commercial experience of doing both styles of software development, the dynamically typed code is the better approach by far.
It's not that I don't understand you, it's just what you are saying is a load of rubbish. :p
So, how often is poorly typed code out there? From the popularity of test coverage tools, it must be ubiquitous.
In a situation where extreme levels of testing occurs, the extra assurance from strong typing is minimal. In a situation where strong typing is enforced, extra testing is still very useful.
Consider a finite state machine with N states. There are a priori NxN possible transitions. In many cases however most of them are impossible, and you really have only O(N) feasible transitions.
Sure if you make O(N^2) tests you don't need typing... but typing could have made many of those transitions literally impossible. You don't need to test the impossible. For a sufficiently large codebase, you want to limit as much as possible the amount of tests you need.
Also I have more than once identified issues in our testing framework because when I made stronger types I uncovered bugs that escaped our tests. Non-deterministic concurrency bugs are extremely hard to test for. So yes, testing can uncover type bugs, but typing can uncover untestable bugs.