What is the difference between Formal Logic and Proofs?

The distinction the author is making is between formal proofs and informal proofs. Most of mathematics is done informally. Informal proofs are just persuasive arguments written in natural language. They are, of course, very stylized, but ultimately it's just an argument. A formal proof is written in a formal language that is in principle (and nowadays in practice) machine-checkable. And for real logics, the algorithm to check such proofs is relatively simple. It is very rare for mathematicians to produce formal proofs, but as tooling for proof assistants improves, largely driven by the needs of software engineering, it becomes more popular.

The social process referenced is presumably processes like peer review and the more amorphous reproving, alternate proofs, alternate explanations of existing proofs that happens as people study a theorem and its proofs. If a bunch of people recheck the work and don't identify any problems, then it's evidence that there aren't any problems. It's clearly not incontrovertible proof that there are no problems.

The following isn't related to your specific question. As Fabio Somenzi points out in a comment, this paper is 40 years old (published in 1979). It's hard for me to imagine someone holding the views given in the quoted introduction nowadays. The reason formal proofs aren't commonly used in software development is that it is perceived (mostly likely, correctly) as not being cost-effective. The main concern that would cause a software developer to not trust some formally verified code is specification error which is not at all helped by using a social rather than mechanical process to verify the proof. It doesn't matter if your theorem is true if your assumptions are wrong. A lot of the impetus for proof assistants (which would have been young or non-existent in 1979) is precisely because informal proofs proved inadequate for verifying software, particularly concurrent software.

1. After reading the paper a bit, I think the autors mean that the proof is more than just the formal logic behind it (they cite Bourbaki):

Indeed every mathematician knows that a proof has not been "understood" if one has done nothing more than verify step by step the correctness of the deductions of which it is composed and has not tried to gain a clear insight into the ideas which have led to the construction of this particular chain of deductions in preference to every other one.

I think I agree unwillingly. When I write formal proofs in Mizar (a proof checker where I do have to go into every last detail) and they become longer than a hundred lines, I feel the need to add extra commentary to give the reader an understanding how the proof works. Shorter proofs are usually self-evident. So I'm doing it myself, yes. But I disagree with the authors that using only formal logic doesn't increase the confidence.

2. If you have a proof for a theorem, but no one reads it, is the theorem really proven for the rest of the world? Mathematicians are, sadly, just humans. When Cantor originally introduced his set theory, he was often frowned upon or simply ignored by the mathematical community. A few decades later David Hilbert said

No one shall expel us from the paradise that Cantor has created.

It is still a problem today. If you prove that, e.g. P=NP, then it will take time for the community to acknowledge the existence of the proof, because from their perspective, there have been so many wrong ones, why should yours, you being an unknown mathematician, be the right one? Fat chance.

The webcomic SMBC has a nice but slightly exaggerated comic about the social process.

Formal logic, and proofs in formal logic, is a game where you encode some symbols and have rules for how you manipulate them.

There is no truth in Formal logic, except how you associate the symbols you write with concepts. Now, those symbols are often designed to align really well with truth, so the two mix relatively well.

The thing is, most uses of "formalism" is very informal. When you define a "formal" model of computation, 9999 times out of 10,000 you talk about it informally. You'll elide or hand-wave some step. Partly because those steps are boring and annoying to formalize, and partly because humans are fallible.

Today we have formal proof checkers. These let you play the formal logic game with a computer-mediated umpire, who takes your proof and makes sure you aren't breaking the rules of the game.

We also have computer proof generating assistants, who can take two assertions you believe are connected and generate a formal proof (the annoying, small steps) that one proves the other, with more or less success.

This is a small corner of mathematics. Most mathematics doesn't use this. Instead of using formal proof checking programs and assistants, they instead write relatively informal proofs. Steps are skipped -- elided -- with the understanding that the reader can convince themselves of the validity of the skipped steps.

Proofs then become a matter of writing for the audience; to consume such a proof, you need to have a certain degree of "mathematical maturity" in the areas covered, or the "A follows B" obvious steps won't be obvious to the reader and everything falls apart.

Often such proofs can be turned into formal proofs, but the process is really hard and long. And sometimes there turns out to be "technical" errors in the proof that need adjusting in order to make the proof formally provable.

In that sense, the formal proofs are stronger than the informal proofs. But in another they are sometimes not.

With the informal proofs, you are often taking the medium-informal definitions involved and a medium-informal statement of the theorem and proving it in a way that is highly convincing to a subject matter expert. What more, the proof itself may contain useful insights into why the theorem is true.

In the formal proof, you are instead taking a specific formal set of terms and definitions and proving them. If those specific formal set of terms and definitions don't align with the medium-informal definitions and statement of theorem, then you can prove something different accidentally. Reliably connecting the computer-understood formal terms to the medium-informal theory and theorem can be a matter of non-trivial effort; in fact, you will probably have to prove they are the same thing, using an informal proof.

Then, the body of the computer-checked proof could be so technical and dense that the "reasoning" could be opaque to the human reader. This is a loss, as often the structure of the proof sheds light on related problems and extensions.

I'll then relate this back to computer software. A formal proof that a program is "correct" then requires that the "correctness" of the program be what the programmer wanted. Expressing that -- what the programmer wants -- is in a sense the problem of programming in the first place!

Programmers create programs that write programs for them all the time.

Every compiler is a program that takes in a "higher level description" of a problem and outputs a lower level description of the problem.

When programmers attempt to create ridiculously high level languages, like the GUI building toolkits, what is universally found is that you lose strength and performance to a huge degree.

Going from C or C++ or similar languages to a gc+bytecode language costs 2x-3x performance; going to a scripting language costs 5x to 10x. Power -- what things you can do -- is also lost (this is typically worked around by having the parts of the program that need power be written in a lower-level language, and access it from the higher level one).

Languages like Java came out of research into writing provably correct programs. Garbage collection and lack of pointer arithmetic and similar make proving properties about the language easier; in comparison, C or C++ has piles of "if the programmer does this, the language makes zero guarantees"; you can write provably correct C or C++, but you end up highly limited in what constructs you can use.

Other languages attempt to give C or C++ levels of abstraction, but add on a proof system to prove that you aren't wandering into the lands of undefined behavior. You can see this in Rust.

But, fundamentally, the entire problem of computer languages and compilers is attempting to do exactly what the formal proof programs in mathematics are doing. They are attempting to allow the author to write a higher level description and have the lower level details handled automatically by a computer.

In short, a sufficiently accurate description of a computer program is a computer program already; saying it is "correct" then becomes checking if the description is correct, which is a problem of meaning not mathematical proof.