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

We run proofs on code all the time, it's called type-checking.

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.

> However the theory itself allows that all code could be mathematically proven

I don’t think this is true, something as “trivial” as halting already can’t be proven in the general case.

But we never need to prove the general case, only specific cases. The general case includes an infinite number of inputs, but in reality there is only a finite number of states a physical computer can have (the number of states far exceeds the number of atoms in the universe, but it is still finite)

I don't think a theoretical computer scientist would agree.

So long as the number of states is finite theory says we can prove by exhaustion. Either a state terminates, or it becomes a different state. Then you do a tree seach until you have reached a termination or a state already in the tree. You need more memory than the number of states to do this, but theroy allows for infine memory in the proof.

Remember the halting problem is proving within a system, we can often step outside the system to prove it. Which sometimes allowes for more properties to be proved'

The halting problem, as I generally think of it, is to receive a program/specification-of-a-machine and output whether it halts. In this formulation, there is no system in which things need proving. Instead, the analogous thing is that, for any program that returns one of “halts”, “doesn’t halt”, or “unknown” and only returns the first two in cases where those are correct, there are other machines which also do that, but where they answer “unknown” for a smaller set of inputs. (E.g. you can just augment the program by hard-coding in the correct value for some input that it previously answered “unknown” for.)

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.

Computer scientists routinely prove theories with an infinite number of states. It is actually usually the easiest way to prove things because you don’t have to handle edge cases.

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.

General case in what meaning? You do have to prove (the interesting properties of) a given algorithm to each possible input, e.g. no one would want to use a sort algorithm that loops forever on a specific list of integers.

And the number of possible states increase so fast that you might as well think of it as infinite.

So long as the list is finite and no being modified outside of sort that can be done for some sort algorithms. Bogo sort wouldn't. If < works as expected (a<b means b<a) most algorithms will sort algorithms terminate, and a few don't even need that (though < working is needed to prove the result is ordered ).

Gödell showed there are algorithms that we cannot prove, but he did that with self referencing algorithms which we rarely use.

Of course the most commonly used CS algorithm is proved correct in various properties, that wasn’t my point.

Still, you can’t even in theory prove every interesting property about any problem/algorithm.

Sure, but i'm contending those algorithms we cannot prove are mostly not used in programming in the real world.