Rust is known for being very "prove it," as you put it, but I think that it is not, and it exposes a weakness in your perspective here. In particular, Rust lets you be lax about types (Any) or other proved constraints (borrow checker bypass by unsafe, Arc, or cloning), but it forces you to decide how the unproven constraints are handled (ranging from undefined behavior to doing what you probably want with performance trade-offs). A langauge that simply lets you not prove it still must choose one of these approaches to run, but you will be less aware of what is chosen and unable to pick the right one for your use case. Writing something with, for example, Arc, .clone(), or Any is almost as easy as writing it in something like Python at the start (just arbitrarily pick one approach and go with it), but you get the aforementioned advantages and it scales better (the reader can instantly see (instead of dredging through the code to try to figure it out) "oh, this could be any type" or "oh, this is taken by ownership, so no spooky action at a distance is likely").
The same is true at multiple levels. `.clone()` is relatively easy to use, although once you learn the basic rules for referencing, that also becomes easier. `Arc` solves a specific problem you run into at a certain point sharing data between threads, but if you're not sharing data between threads (and most of the time you're not), it's just boilerplate and confusing, so you might avoid it and at worst use `Rc`. `Any` is rarely an obvious choice for most contexts, you really are going to only use it when you need it.
The result is that for most simple cases, the precise and "proven" option is typically the easiest to go for. When you deal with more complicated things, the more complicated tools are available to you. That seems exactly what the previous poster described, where you can decide yourself how much you need to prove a given thing.
This was my biggest problem when I used to write Rust. The article has a small example but when you start working on large codebases these problems pop up more frequently.
Everyone says the Rust compiler will save you from bugs like this but as the article shows you can compile bugs into your codebase and when you finally get an unrelated error you have to debug all the bugs in your code. Even the ones that were working previously.
> Rust does not know more about the semantics of your program than you do
Also this. Some people absolutely refuse to believe it though.
However, you've still got to do that job of encoding the semantics. Moreover, the default semantics may not necessarily be the semantics you are interested in. So you need to understand the default semantics enough to know when you need something different. This is the big disadvantage of lifetime elision: in most cases it works well, but it creates defaults that may not be what you're after.
The other side is that sometimes the semantics you want to encode can't be expressed in the type system, either because the type system explicitly disallows them, or because it doesn't comprehend them. At this point you start running into issues like disjoint borrows, where you know two attributes in a struct can be borrowed independently, but it's very difficult to express this to the compiler.
That said, I think Rust gives you more power to express semantics in the type system than a lot of other languages (particularly a lot of more mainstream languages) which I think is what gives rise to this idea that "if it compiles, it works". The more you express, the more likely that statement is to be true, although the more you need to check that what you've expressed does match the semantics you're aiming for.