What to prove and how to prove it

Question

In learning about proof theory, I am interested to know how to go about "proving properties of a program". I don't exactly see yet what needs to be proven, nor how to prove it, which leads to this brief discussion followed by some questions.

In some languages (such as TLA+), the program is the specification (I think). If not TLA+, maybe you can do that in Coq, but I've heard of it. So that means roughly that what you write is automatically proven. But if that is the case, how do you prove that it's proven. It seems that at some point you have to actually test both the code and the proofs and see that it does what the specification says. Some basic TDD.

In reviewing the Curry-Howard correspondence, programs are proofs, or at least lambda/functional/logic style programs. Not really sure what this means in practice. If simply writing a new function that implements a specification means we have a proof, or what.

So the questions are:

1. What exactly we are proving.
2. How do we prove that the system meets the specification (if the language is or is not the actual specification). If I write code that says "I will always handle this HTTP request error by tracing its output to the console", and that is "specified" in the specification, then how does it get proven. Not sure what I do to say "guaranteed, this behavior will happen". In my head the only way this can be proven is by actually doing tests on the code (i.e. model testing or just brute force simulation testing like you would see in TDD).
3. When writing tests (as in TDD) comes into play when creating these proofs. Wondering if proofs need tests, sorta thing, or at what point you are done with your proof being proven.

So it seems that what we want to prove is that the system behaves as expected. And given we have defined how we want the system to work, the question is how to prove it matches the specification, at a high level. How much do we prove, how do we know the proofs actually prove what we want and the behavior will be what we want (and proven).