Contracts are annotations, much like types are. What makes contracts powerful is the tool that examines this annotation, as is the case with types. A type checker, such as an H-M type checker, can only perform limited checks. It's possible to use a dependent type checker with dependent types, but this is undecidable, and it requires a proof assistant and human guided tactics to resolve. In practice, this is expensive, and when automation such as LLMs are used, one currently gets tactic soup that is difficult to understand, which defeats the purpose.
A model checker, such as CBMC or ESBMC, can work with contracts to verify specification that would be difficult to verify without contracts. Model checkers can already verify memory safety and even the absence of memory leaks across an entire program. However, model checking grows exponentially expensive as we add more code to be verified. Contracts give us the ability to perform compositional verification, which allows us to verify codebases into the millions of lines of code or larger by breaking down this verification into many small model checks, stitching these together with contracts and invariants. Contracts and invariants complement type checking and significantly extend it. It's possible to use contracts and invariants to add these checks to an untyped language or a minimally typed language such as C. If my precondition includes the data invariant, "property_valid_widget(x)", then effectively, this also type checks x. This works even if I've completely erased the type and later recast it.
The "real world" doesn't currently have a solution for reducing general software safety issues -- which goes far beyond memory safety -- other than formal methods. Practical and efficient ways to formally verify software is within our reach, and is already being done with other languages. I do this today with C / CBMC using contracts and invariants. I get memory safety, specification safety, and a guarantee of no memory leaks. This can also be done with C++, Rust, Java, and other languages using similar techniques. While it is true that Rust and Java both have basic memory safety in place, they also both can harbor vulnerabilities that could be resolved with function contracts and model checking.
Contracts are more than useful; they give visibility of developer intent to model checkers and similar tools. This visibility makes software significantly safer than borrow checking or type checking can alone.