> So proofs and programs are isomorphic. We know there are programs which never halt and we know there are programs for which we can not algorithmically decide whether they halt or not. What is the equivalent thing in proofs? Are there proofs which never halt?

Yes; a "proof which never halts" is an invalid attempt at a proof (so not really a proof).

To a first approximation, the Curry–Howard correspondence says that programming and proving are the same. This is literally true if "programming" and "proving" are restricted to mean more specific things. (There are many variants of the Curry–Howard correspondence. The simplest one relates "simply-typed lambda calculus" with "propositional intuitionistic logic". Simply-typed lambda calculus is basically what you get when you take Python, strip everything away except for the keyword "lambda", and add types. Intuitionistic propositional logic is basically what you get when you take ordinary logical reasoning, strip away quantifiers ("for all", "there exists") and force yourself to never use proof by contradiction. There are also variants for more powerful programming languages and more powerful logics. The case of classical logic, where we can use proof by contradiction, is particularly interesting, since the translations of such proofs make use of continuations. See https://rawgit.com/iblech/talk-constructive-mathematics/mast...) But in a wider sense it's false: Invalid proves aren't very much worthwhile, while non-terminating programs can be. Thus a better approximation is "programming strictly encompasses proving".

> Is a proof really isomorphic with a program as written in source-code, or is it isomorphic with the EXECUTION of a program with a given input?

The former.

> A program and its execution are not the same thing are they?

Correct. A program is a piece of a text. Its execution is (for me, in this context) the final value computed by the program. (The Curry–Howard correspondence is easiest to understand when we restrict to programs in a purely-functional programming language like Haskell.)

> But with proofs I find it hard to think about the difference between the "source-code" of a proof and the "execution" of a proof. Is there such a thing as distinction between the execution of a proof and the "source-code" of it?

I'm with you; the reason the difference is hard to see is because while we run programs all the time, we almost never run proofs. However, yes, indeed, you can run proofs. The result will be a "proof certificate", something like a proof with all intermediate definitions unrolled and then maximally simplified.

Quite different-looking proofs (texts) can yield the same "proof certificate" when ran, exactly as different-looking source codes can yield the same final value when ran.

Here is an example. Consider the following proof (due to Euclid) of the fact that there is a prime number greater than 6: "Like any positive natural number, the number N = 1⋅2⋅3⋅4⋅5⋅6 + 1 is a product of prime numbers. However, no number between 2 and 6 is a factor of N, since dividing N by any such number will always leave a remainder of one. Hence all the prime factors of N, for definiteness pick the smallest one, are prime numbers greater than 6." The proof certificate obtained by running this proof will be the pair (7,...), where "..." is a certificate that the number 7 is indeed prime. The reason the number 7 appears here is because 1⋅2⋅3⋅4⋅5⋅6 + 1 = 721 = 7 * 103. If the proof picked the largest factor instead of the smallest, the result of the proof would be the pair (103,...) (with a different primality certificate).

Running proofs is becoming a more important thing nowadays, thanks to the development of good proof assistants and homotopy type theory. (While in principle it's possible run proofs manually, like in the previous paragraph, it's only fun when a computer does it for you.) For instance, a mathematician might prove that some particular structure of interest only contains finitely many elements, without having a clue how many values there are. If she runs the proof, the computer will tell her the answer. The catch is that with current (mathematical) technology, she might have to wait quite a bit for the answer. (The in my circles famous "Brunerie two" comes to mind: This is a proof where we know the answer to be the number 2, and made much progress in pimping the Curry–Howard correspondence, but aren't quite there yet. See https://guillaumebrunerie.github.io/pdf/cubicalexperiments.p...)