[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.