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)?
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)?