If I am trying to prove something I can state in my target language how would statement and proof differ?
If the thing to prove is not expressible in the target language (e.g. the fact that a function terminates) I would have to use a separate language anyway.
Could you give an example how this could hypothetically look like (preferably in pseudo Rust)?
1) you might have two algorithms for computing the same thing, one simple and obviously right, and one complex and optimized. So you want to state that they always produce the same thing.
fn my_complex_algo(x : Input) -> o:Output ensures o == simple_algo(x)
3. You might have really simple properties you want to prove, for example that an "unreachable!()" is indeed actually unreachable.
Right. Those are the kinds of systems that are easy to specify concisely. Databases, for example, can be specified as giant arrays with linear search.