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.