Where the type system isn't that expressive, you still have to fall back to testing to fill in the places where the type system isn't sufficient, and your tests are also going to 'deal with "what if this input is null?" everywhere' cases and whatnot by virtue of execution constraints anyway.
I'm not sure I agree with your prior that "your tests are also going to 'deal with "what if this input is null?" everywhere' cases and whatnot." Invalid input is at the very edge of the program where it goes through a parser. If I parse a string value into a type with no room for null, that eliminates a whole class of errors throughout the program. I do need to test that my parser does what I assume it will, sure. But once I have a type that cannot represent illegal data, I can focus my testing away from playing defense on every function.
I can confirm that at least 30% of the prod alerts I've seen come from NullReferenceExceptions. I insist on writing new C# code with null-checking enabled which mostly solves the problem, but there's still plenty of code in the wild crashing on null bugs all the time.
Of those who are concerned about type theory? 99%. With a delusional 1% thinking that a gimped type system (read: insufficient for formal proofs) is some kind of magic that negates the need to write tests, somehow not noticing that many of the lessons on how to write good tests come from those language ecosystems (e.g. Haskell).
> I can confirm that at least 30% of the prod alerts I've seen come from NullReferenceExceptions.
I don't think I've ever seen a null exception (or closest language analog) occur in production, and I spent a lot of years involved in projects that used dynamically typed languages even. I'd still love for someone to show actual code and associated tests to see how they ended up in that situation. The other commenter, despite being adamant, has become avoidant when it comes down to it.
The "how" is almost always lack of discipline (or as I sometimes couch it, "imagination") but usually shit like https://github.com/microsoft/SynapseML/issues/405#:~:text=cl...
I've had to learn in my career not to open other people's projects in a real IDE because of all the screaming it does about "value can be null"
There is admittedly a lot in the update and I may have simply missed it, but I don't see any modifications, even additions, to tests to denote recognition of the problem in the earlier version. Which, while not knowing much about the project, makes me think that there really isn't any meaningful testing going on. That maybe be interesting for what it is, I suppose, but not really in the vein of the discussion here about where one is using type systems and testing to overcome their personal limitations.
Yeah, when you have extra tools like that it can certainly help. The thing is that you can ignore any warning! I like it to be a compiler error because then there's no way to put that on the tech-debt credit card and still pass CI. If you are able to put those warnings into your CI so a PR with them cannot merge, then that's like 99% of what I like in my code: make the computer think of the low-hanging-fruit things that can go wrong.
With all of that said, solving for null does not get you everything a tagged union type does, but that's a different story.