Sorry that this is a very basic question but I never had any of this in uni and I find it super exciting:
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)
2. You might have high level "properties" you want to be true about your program. For example, a classic property about type-checkers is that they are "sound" (meaning that if you say a program is well typed, then when you run it it must be impossible to get a type error).
3. You might have really simple properties you want to prove, for example that an "unreachable!()" is indeed actually unreachable.
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)?