Racket goes a step further from having types and gives you contracts. The whole language is defined by these contracts. For example,
> (list 1 2 3 4)
is a way to create a list consisting of elements 1, 2, 3, and 4. This procedure is defined as returning a `list?` (a contract checking for a list) and the values provided are `any/c` (a contract representing any value). But many other languages can support something like that just fine. Where contracts further help are with composition and specifying allowable values or ranges of values. For example,
> (round 2.4)
2.0
as we expect. But looking at the definition of `round`, we see that `(round x)` accepts an `x` satisfying contract `real?` and returns `(or/c integer? +inf.0 -inf.0 +nan.0)`. If you try to `round` Infinity or NaN, you get what you "expect" and not some new value. If you try to `round` POSITIVE_INFINITY in Java, you'll get
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.
