[the_af]

> I literally have piles of boolean-typed functions in business logic

Yes, but this is working with legacy code that wasn't written with a mature type-checking system in mind. The boolean type encodes very little meaning with it, and so there's not much you can reason about it, as you've noticed.

If your argument is "a modern type system cannot help me much with legacy code that didn't leverage it to begin with" I can understand you and even agree somewhat. But that's a different argument.

That's what I mean by circular reasoning: if you don't use the types, then yes, a type system won't be of much use. You'll spend time writing unit tests, which for legacy code seems like an adequate approach.

[dragonwriter]

If your type-checker is “mature" enough to encode the full value level semantics of the code it types (rendering the code itself superfluous, as then you’d just need to compile the type-level code to get your app), you then have the problem of validating the logic of the type-level code, and the natural solution to that problem is, again, testing.

[the_af]

Type checking is modeling + testing.

[gleenn]

I neither used the word legacy nor modern. I don't care how fancy your type checker is today or tomorrow, the arbitrarily deeply complicated boolean-typed function I write tomorrow gleans nearly zero value from type validation. It gains actual validation of correctness with real tests.

[the_af]

It's a legacy problem in the sense your system is a badly designed mess of functions that only return boolean. You could encode additional semantics in the types. Of course if you don't, the type system will be unhelpful.

This is a modeling problem at this point. Types can make your model better by encoding more things. It's often not easy or feasible to refactor the mess, so sometimes you're stuck with it.

[gleenn]

Can you explain concretely how adding types would make a bunch of boolean-valued functions and some tests better? What types would you introduce to my example?

[ninetyninenine]

You need dependent types for this to fly. But the main argument is that there’s an infinite number of ways your Boolean functions can go wrong if they mistakenly taken a wrong input type or return a non Boolean. Types reduce this universe of runtime errors by 99 percent. It’s still infinite though but you have a lot less possible errors.

[gleenn]

That's my point, the type errors being reduced isn't that interesting, I usually find and fix those extremely quickly. What I don't find but am most interested in is the actual logic. So I must write tests. And when I write tests, I get the type errors covered too. So why should I spend my precious time modeling inside a type system when the ROI is minuscule and the cost is I have to litter my codebase with types. Just write the tests.

[ninetyninenine]

You can write the test in the type system with dependent types. It's the same thing. But your language needs to support this. Typescript supports it. The static analyzer in your ide or during compilation will now run the test. You get a model and a test for free.