contracts are still runtime checks and thus different from a static type system, which gives you a proof, ahead-of-time, that your program will be well-typed no

contracts are still runtime checks and thus different from a static type system, which gives you a proof, ahead-of-time, that your program will be well-typed no matter the input (well, at least in theory - in practice, many type systems are unsound, but it takes some effort to actually break the system). you're right that a contract allows you to specify more precise properties than a "regular" type system, but it comes at the aforementioned cost. If you want both, dependent types would be your best bet, but those are... rather complex in practice and to my knowledge, not really "production-ready". as for your example though, it would be possible to implement `Math.round()` in such a way in Java that it doesn't just return an int, but some sum type that encodes whether it's an actual result or some invalid value. The reasons why this isn't done are probably a) it's awkward, though possible, to express sum types in Java (this would be easier in some other languages), b) it would force the caller to always have to explicitly consider the case that the value is invalid even when they know it's not, making mathematical calculations tedious and hard to understand.