While the barebones aspect of Lisp is appealing, there is no way I will commit again to a language that's not statically typed.
There is a difference for a language between "readable" and "understandable".
To me, languages that don't have type annotations (ideally with type inference) might look pleasing to the eye but they are a nightmare to maintain and modify because so much vital information is missing.
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.
You can write a lisp that uses static typing. The book "The Little Typer" develops one such language as (I believe) a dialect of Scheme. Of course, that's just a toy language (and it doesn't have type inference, for example, but as far as I'm aware that's a hard problem when you add dependent types), but it shows it can be done.
There is a difference for a language between "readable" and "understandable".
To me, languages that don't have type annotations (ideally with type inference) might look pleasing to the eye but they are a nightmare to maintain and modify because so much vital information is missing.