[goostavos]

Alas, the problem with java, which I say as a begrudging long time java developer, is that "supports this distinction" is a theoretical benefit that is seldom used in practice. Checked and unchecked exceptions get so thoroughly abused and twisted into byzantine contraptions that any distinction, if value were to be gained from it, is completely destroyed by the common free form usage throughout the ecosystem.

The precondition thing, while indeed common, drives me sorta insane. I think it's a pattern java folks need to move on from. You've got this lovely type system (used loosely). If you need a precondition because you've got some fundamental invariant in the system, doing it at runtime rather than encoding it into the type system is such a missed opportunity. If I try to do something inherently wrong, I don't want the code to even compile!

[yCombLinks]

What kind of precondition and what kind of example do you have for the typing? My primary precondition is null checks, which is unavoidable

[goostavos]

This blog post really captures the core of where null checking should go and how to capture that you've already vetted this field for correctness in the type system so that the rest of your code never has to worry about it -- and further, cannot because the types don't allow!: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

This is echoed in an amazing book called Domain Design Made Functional, which radically changed how I thought about what a type system is and what it can actually do for us if we lean on it correctly (even a relatively crummy one like Java's!).