It also isn't clear that the machines itself actually do what they say, though hardware is a lot more likely to be mathematically proven.
Maybe that's a nitpick, but I would say it's fundamentally impossible to mathematically prove anything at all about a physical system. You have to assume some model to do the proof and have no way of ever "proving" (what would that even mean?) that model.
I guess you're referring to the fact that verification and formal methods are used in hardware more often than software. This is due to commercial reasons: you can't just reprogram a million chips once they leave your fab.
What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.
I don’t think this is true, something as “trivial” as halting already can’t be proven in the general case.
Of course, what you are saying about “stronger systems can prove the answers to the questions of the whether the machines from larger sets, halt” is also true, I just, wouldn’t describe this as “the halting problem”, even though they are I guess basically equivalent.
A typical theory says:
For all x:A, P x
In other words, given any x (from an infinite set A) P x is true. Where P is a proposition.
You typically prove it using straightforward induction/recursion.
And the number of possible states increase so fast that you might as well think of it as infinite.
Gödell showed there are algorithms that we cannot prove, but he did that with self referencing algorithms which we rarely use.
Still, you can’t even in theory prove every interesting property about any problem/algorithm.
In principle, nothing prevents you from taking e.g. an ARM binary and formally proving that it will never crash in some environment, e.g., bare metal chip with known amounts of memory etc. This is very hard for useful programs and not worth it in pretty much any application there ever was, but it's possible and getting ever easier over time.
As a sibling comment observed, you would be proving something about a program, but proving things about programs is both possible and done.
This ranges from things like CakeML (https://cakeml.org/) and CompCert (compilers with verified correctness proofs of their optimizations) to something simple like absence of runtime type errors in statically strongly soundly-typed languages.
Of note is that you are proving properties of your program, not proving them perfect in every way. The properties of your program that you prove can vary wildly in both difficulty and usefulness. A sufficiently advanced formally verified compiler like CakeML can transfer a high-level proof about your source code to a corresponding proof about the behavior of the generated machine-executable code.
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.
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.
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.
"One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox."
This is similar to constraints of making something semi-decidable or recursively enumerable.
Provable, recursively enumerable, semidecidable, and turing recognizable are all the same thing described in different ways.
Some things are easier to find in type theory, other in set theory and for some Turing machines work better.
The Church–Turing thesis isn't provable but is the safe assumption.
IMHO termination analysis, which will never be complete, has more interesting and has some implications for ATP that aren't as easily captured in type theory.
As an example related to term rewriting which will be important to ML.