> The compiler does not and cannot check if these strict requirements are enough for the intended "safety". Right? It is the judgement of the programmer.
Yes*. It's up to the programmer to check that the safe abstraction they create around unsafe code guarantees all the requirements the unsafe code needs are upheld. The point is that that's done once, and then all the safe code using that safe abstraction can't possibly fail to meet those requirements - or in other words any safety related bug is always in the relatively small amount of code that uses unsafe and builds those safe abstraction.
> And what is stopping a `c` function with such requirements to be wrapped in some code that [doesn't] actually checks these requirements are met?
Assuming my edit to your comment is correct - nothing. It's merely the case that any such bug would be in the small amount of clearly labelled (with the unsafe keyword) binding code instead of "anywhere".
> The only thing that the rust compiler enables is to include a feature to mark a specific function as unsafe.
No, the rust compiler has a lot more features than just a way to mark specific functions as unsafe. The borrow checker, and it's associated lifetime constraints, enforcing that variables that are moved out of (and aren't `Copy`) aren't used, is one obvious example.
Another example is marking how data can be used across threads with traits like `Send` and `Sync`. Another - when compared to C anyways - is simply having a visibility system so that you can create structs with fields that aren't directly accessible via other code (so you can control every single function that directly accesses them and maintain invariants in those functions).
> In both cases there is zero help from the compiler to actually verify that the checks that are done on top are sufficient.
Yes and no, "unsafe" in rust is synonymous with "the compiler isn't able to verify this for you". Typically rust docs do a pretty good job of enumerating exactly what the programmer must verify. There are tools that try to help the programmer do this, from simple things like being able to enable a lint that checks every time you wrote unsafe you left a comment saying why it's ok, and that you actually wrote something the compiler couldn't verify in the first place. To complex things like having a (very slow) interpreter that carefully checks that in at least one specific execution every required invariant is maintained (with the exception of some FFI stuff that it fails on as it is unable to see across language boundaries sufficiently well).
The rust ecosystem is very interested in tools that make it easier to write correct unsafe code. It's just rather fundamentally a hard problem.
* Technically there are very experimental proof systems that can check some cases these days. But I wouldn't say they are ready for prime time use yet.