Ah well but that’s kind of impossible. The reason tests can provide a stronger confidence is that they actually run the code. Wheras the type system only “looks” at the code and tries to make predictions from that. It’s fundamentally hard because the halting problem is in the way.
Before someone jumps in here and says: what about dependent types. Well yes if your type system is Turing complete in itself like e.g. the Dependent Types of Idris they you can write your property based tests in the type system and run them at compile time. This is no different to writing tests except for the language you write them in. I’d rather code QuickCheck tests in Erlang than property based tests in the Idris type system.
So (non Turing complete) type systems can never find everything tests can find. And in practice they don’t get even close. After all QuickCheck was initially implemented for Haskell … if static types are so good why would someone need tests still? Because types only look skin deep.
It’s hard to quantify lines of code, we basically have a large set of libraries used by multiple products, and the main hilarity would be when we’d get a feature request for something that had happily been running in production for half a decade without any support being needed (gee, thanks Erlang) and then suddenly either have to work against the old versions of those libraries or take the plunge and upgrade. You’re probably talking a couple hundred thousand line of code being used by a dozen or so products with their own hundred thousand lines of code. (A quick scan with cloc across a few of them would indicate this is the case).
A lot of issues can be ameliorated through the judicious use of Dialyzer as previously mentioned, further issues can be avoided by writing code that’s as easy to throw away as it was to write in the first place (A very common solution!).
The bite really comes in shared code that we can’t develop as a discrete chunk of code that could be worked on in isolation - for example, we work in the media streaming space, therefore we have the general concept of a ‘frame’, that surprisingly enough most of the code with (to lesser or greater degree) uses. A change to that structure would incur sweeping changes across the code-base, the vast majority (by design) would then incur compile-time errors - a decision we made by deliberately using shared records in header files. We could have avoided that by using independent data structures per module and mapping - but that’s expensive at runtime and to be avoided with such a central concept as this.
I wouldn’t lay the blame at Erlang’s feet for a lot of this - it is the type of thing that’d happen across any code-base where you have a large central domain by the very nature of that domain - but moving to a typed language makes that much easier to reason about.
That’s not to say some lessons haven’t been learned - more tests, and treating those core libraries as something that need versioning as a product in their own right will make life easier going forwards, and that’s got nothing to do with the language either.
I’m sure you heard of coverage measurement during testing. Tests can look as deep as you want them too. And I was explicitly talking about property based testing with QuickCheck, what can be achieved there is way beyond skin deep and way beyond what any static types (with the disclaimer of tests written with dependent types which are a mere academic experiment currently).
When I was developing my own language I looked at all kinds of type systems including something which would be called dependent types nowadays. Nothing gave me sufficient quality assurance to be used in safety critical systems I was working on back then. It’s simply not possible (see halting problem argument above) without running code i.e. testing.
Then I discovered Erlang with its pervasive runtime checking due to pattern matching and coupled that with fault tolerance and had to admit myself that this is the language I should have developed. Since then I try to add the missing pieces I had in my design to Erlang (mainly around hard realtime and a few other concepts). And there are none of my type system ideas I would want to add.
All I want to get people aware: there is a price to pay for static types and the gains are in principle limited. No theoretical limits for what can be achieved with through and methodically advanced testing.
I think this is just where we’ll disagree. I think static analysis free (once you learn how to use them), but tests you have to work on forever (once you’ve learnt how to use them).
I’m very lazy, so I prefer static analysis of the two, and I opt for snapshot tests primarily as I find they have the lowest maintainence cost of all the testing strategies I’m familar with.
I think those are all simplifications of the actual problems both approaches have and that you will find in codebases.
If you take the simplest function, &&, with type bool -> bool -> bool, a type system won’t catch a faulty implementation (unless it provides singleton types, dependent types, etc). A unit test may not cover all cases nor test all branches (unless you are doing branch coverage, concolic testing, etc). Therefore I am not surprised there is distrust on both sides when the most common usage of those techniques are not sufficient for a function that you learn during your first week of CS.
Honestly, if I were to jump into a codebase that has types but has no tests, I would be horrified of making any change. It is like buying a car with no warranty the engine will actually turn on (but rest assured it is a car). In exactly the same way that code coverage does not guarantee you actually tested something (only that those paths were executed without errors).
PS: I would be even more horrified of a codebase that has no types and no tests.
