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.
So, how often is poorly tested code out there? From the popularity of strong static typing, it must be ubiquitous.
Strong types aren't just a correctness guarantee, they also help to discover structure and interfaces that previously were implicit.
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.
That is a very original take, but I think you have it reversed. Typing removes the possibility of _some_ errors. Those are tests you do not _need_ to write (you can still write them if you want), thus having more time and attention to write tests that matter. Typing is a baseline, and anything over that baseline you can deal with 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.
You seem to be thinking that testing for type errors is something additional to general testing. It's not. With sufficiently strong logic testing, the testing for type errors comes along for free.
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.
The point of static typing is that the compiler does checks before your program even starts. And that avoids to write lot of coverage tests that are needed (but usually just ignored) with languages that massively use loosely typed data containers (variables).
Sure, if you're going to be in an environment where the code is going to be bad because of inadequate testing (and I admit this is quite common, due to the cost of the testing needed), static typing lets it be somewhat less bad. It's just important to understand it's a band-aid, not a panacea.
Static typing, as done in mainstream languages, doesn't show your program is correct. Is you compiler written in a mainstream language correct just because it compiles? Of course not. Don't point to academic curiosities with dependent types if they aren't actually used. Extensive testing, on the other hand, is used in the "real world" for assurance.
Every code out there on the real world is full of baindaids and duct tape. Yet, the actual amount varies a lot, as does the centrality of the patched things.
Integration tests are different, but I tend to believe that a strong enough type system should be able to negate the need for unit tests completely.
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.
When I say adequately tested, I mean much more than unit tests. Unit tests aren't going to give you bulletproof code. They don't detect bugs that arise from interactions at a higher level.
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.
Unit tests and types solve somewhat different problems. You can force a unit test to check everything a type system does with effort (mostly by throwing wrong types at your API and verifying you get an error), but I'm not sure how you would use the type system to enforce sort() actually sorts. Sure sort can take a listOfFoo and return a sortedListOfFoo - but that doesn't verify sortedListOfFoo is actually sorted - and in many cases I want an API that is find with listOfFoo but should handle sortedListOfFoo as well.
With dependent types you can encode any proposition in first-order logic (?). You can indeed define an array type that is necessarily sorted. It won't be pretty but it's possible.
I like type systems as much as anyone but I can't see how your type system will check that sin(pi) == 0
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.
> 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.
Ok, but it's cheaper to not have to write those tests than it is to write those tests.
Yes. It's cheaper to have a lower assurance your program is correct than to have a higher assurance. The claim I'm making is that at the high end, the extra assurance from strong static typing becomes minimal.
Yeah, big piles of untyped Django spaghetti need a behemoth suite of integration tests in order to remotely approach the sort of runtime guarantees that typed languages give you for free.
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...
If you adequately test your code for logic bugs, you test the type correctness for free. So, yeah, writing those logic tests is hard. But at least they are finding bugs that static type checking never will (absent the unrealistic scenario of proving your program correct via a type system.)
(It won't find latent bugs that can't currently be exercised, so the testing can't be one and done.)
you can't ensure that you hit every possible case in your test suite. type errors can still slip through in production, just like logic bugs do. it happens all the time in real-life code. that "adequately" is a no-true-scotsman.
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.
You are assuming type errors are caught by tests explicitly written to detect them, as opposed to being found by other kinds of tests. For example, property based tests, with automated generation of inputs to a program or module, don't explicitly test for type errors, but are still (in my experience) quite good at hunting them out.
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.
>You are assuming type errors are caught by tests explicitly written to detect them, as opposed to being found by other kinds of tests.
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?
"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).
>Because type errors in unit tested code are basically non existent.
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.
Sadly, it still took 4 days to clear the deadlocks out of my Rust program.
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
No. It is useful in almost every environment other than things like REPL. I can write TypeScript for hours without writing any tests, run it and fix a few minor logic bugs and code is production level, which is great for prototyping. No chance with plain JavaScript without typing -- it would be at least a day or two and I would constantly run into stupid typos or other errors that can only be found at runtime.
Good tests only render SST superfluous insofar as the person writing the tests is capable of never making a mistake. The thing about good static type systems is they don't typically make mistakes in the domain they work in. The fact that you don't have to muddy your test with a bunch of type checking logic and instead focus on the thing actually being tested is just the cherry on top.
High test coverage is useful in the environment where the code is not adequately typed. That's because static types adequate to make the code bulletproof will also detect the problems unit tests could detect, rendering high unit test coverage superfluous.
So, how often is poorly typed code out there? From the popularity of test coverage tools, it must be ubiquitous.
The turned-around argument has a problem: testing should reveal type bugs, but static typing (of the kind typically discussed for mainstream languages) can't reveal non-type bugs.
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.
I don't think it's possible to test a sufficiently complex system that isn't somewhat restricted in the states it goes through, which requires typing.
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.
So, how often is poorly tested code out there? From the popularity of strong static typing, it must be ubiquitous.