[phplovesong]

For example if a have a type with 3 constuctors, and later one new dev adds one more case and forgets to handle it in every call site. No test will catch this 100%, but something like ocaml will just by compiling the program.

I know fo is not (i dont want it to be) like ocaml, bit any modern language should have some of the basic safety features baked in.

[9rx]

> later one new dev adds one more case and forgets to handle it in every call site

Okay, so you are dreaming of a situation where you allow a new developer who doesn't know anything about how to engineer software unfettered access to your codebase and he goes in and starts mucking about to where he ends up doing things that no sensible human would ever consider acceptable?

I accept you like to live dangerously and have no real care for the product you are building. But, still, you've only covered a limited subset of all the similar things this new developer who doesn't know the first thing about building software can make a mess of. Ocaml just isn't going to cut it.

To reach the full gamut you need, say, a proper dependent type system. But are you really going to throw all your Ocaml code away and start writing Rocq just to deal with this guy you should have never let touch your code in the first place? Probably not. So, what now? Your only practical option is to fire him and find someone who actually understands how to write software. And at that point your tests will catch such forgetfulness just fine.

> No test will catch this 100%

Testing cannot exhaust all cases where the search space is infinite as that requires infinite time to evaluate. In this case, you have exactly 4 states. That is evaluated on the order of nanoseconds. If your tests are not capturing every one of those four permutations, it seems clear that you need to stop letting any random Joe who has never done more than some quick vibe coding anywhere near your code. These are solved problems.

And, hell, even if you did switch to a language with a proper type system, like Rocq, so you could mathematically guarantee all aspects of your program, the shitty programmer will still fail to write theorems that are free of holes. So don't think that even lets you of the hook in hiring those who live by the vibes. There is simply no escaping the need for solid engineering.

When you have that, exhaustiveness checking still remains a useful tool, but you aren't going to forget something and ship broken code to production if you don't have it. This isn't a realistic scenario outside of the contrived. Again, The construct is useful enough that you don't need to oversell it on imagined hypotheticals.

[phplovesong]

> Okay, so you are dreaming of a situation where you allow a new developer who doesn't know anything about how to engineer software unfettered access to your codebase and he goes in and starts mucking about to where he ends up doing things that no sensible human would ever consider acceptable?

Tell me without telling me you have never worked on a large scale business app.

[9rx]

I did long enough to know that in large teams you won't find many accepting of usable type systems. For the same reason the blub developer cannot write good tests, if they can figure out how to write tests at all, they equally fail with types. Which makes sense — testing and types try to solve the exact same problem. The mindset required to grasp and be productive with both is identical. So your imagined hypothetical doesn't even work there. These large scale apps of which you are speak are simply built around constant failure in production. If it is good enough for GitHub...

The only place where the your contrived idea is in any way plausible is where you have a solo developer who thinks he is able to write code without making mistakes or needing to document anything, using a half-assed type system not failing as some kind of proof to himself of that. But in reading this he, unless the hubris is completely off the charts, will be reevaluating that stance.

[phplovesong]

> you won't find many accepting of usable type systems

I think its not about the "typesystem" but the fear of using something the dev is unfamiliar with. I know people who has written the same code, in the same language for 20+ years. "It worked then, and it will work now" is tattooed on their forehead. Its basic human behaviour, you see this in politics, business and life in general.

> testing and types try to solve the exact same problem

Sure, they overlap.

Tests are just a poor mans types, Types are just a poor mans tests

But in my mind tests cover the how, and types the what. With both you need less of both. Its a win-win.

> These large scale apps of which you are speak are simply built around constant failure in production.

This is true. But im going to my grave trying to change that. Its an uphill battle.