[mapM]

I think you misunderstand. On your point about programs not being "provable": it is certainly possible to prove some properties about some programs. It is not necessarily easy, and it very much depends on the program and the property in question, but it is possible.

However, this is not what the article is about. Instead, it talks about an interesting observation that there is a direct correspondence between a certain kind of program and a mathematical proof, and also between the type of the program, and the theorem validated by the proof. In other words, you can think of mathematical proofs as computational objects. The intuition for the correspondence is not hard: for example, support I want to prove that "if A is true, then B must also be true". You may think of a proof for such a property as a program, which takes as input a proof that `A` holds, and as its output produces a proof that `B` holds.

[nyrikki]

Entscheidungsproblem, the Halting problem, the total function problem, etc... typically relate to arbitrary programs.

The point being is there is no single general algorithm that can solve them.

The example you gave above is propositional logic, or zeroith order logic which is known to be decidable.

First order logic and higher order logic are not decidable.

Total functions are also not subject to the halting problem, but unfortunately finding a total function in the general case is also undecidable.

[deterministic]

It doesn’t matter. What matters is if you can prove things you care about true for code you care about.

And yes we can prove termination and zero bugs for a lot of practical useful code. Examples: seL4 is a proven correct micro kernel and CompCert is a proven correct C compiler.

The trick is to use programming languages that are total i.e. not general infinite tape turing machines.