Beware of Cranks: Misguided attempts to solve impossible mathematical problems

>Even the halting problem is easily solved in practice.

no, it's not. Knowing that this specific program halts or not doesn't address the issue.

Thats when you say sure well start a basic research lab that will be $100 mil per year

> In fact, members of the academy were so tired of being inundated with quackery that in 1775 they passed a resolution not to accept solutions to the problems of circle squaring, angle trisection, or cube doubling.

This is hilarious.

The "compass" and "straightedge" are (nowadays) just a colorful/concrete way to describe the problem. When mathematicians consider this, they phrase the conditions in such a way that no physical "compasses" or "straightedges" are involved.

For example, you might say: (1) If you have 4 different points P, Q, R, S so that the lines PQ and RS are not parallel, you may "acquire" their point of intersection; (2) If you have 4 different points P, Q, R, S and the circle with center P and radius PQ intersects the line RS then you may "acquire" the point(s) of intersection of the circle and the line; (3) If you have 4 different point P, Q, R, S and the circle with center P and radius PQ intersects the circle with center R and radius RS, you can "acquire" the intersection point(s) of the circles. ("Acquire" a point means roughly that your number system now contains the coordinates of the point.)

Notice that this removes the problem of people doing unintended tricks with or drawing horribly complicated diagrams with physical compasses or straightedges, and makes mathematically precise what is allowed.

The following is probably more than you want to know, even though I'll omit lots of the details. The idea is that circles are defined by quadratic equations, and lines by linear equations. At every step, you're solving (acquring the roots of) simultaneous linear or quadratic equations. Starting with the rational numbers, as you "acquire" new points, you "extend" the rationals to bigger fields "by extensions of degree 1 or 2". Since degrees multiply, at any point, you've "extended" the rationals by a total degree 2^n.

So the result is: Theorem. Any point you construct must (a) lie in an extension of the rationals of degree 2^n; (b) be algebraic, in the sense that its coordinates are roots of rational polynomials.

Now take something like trisecting a 60 degree angle. A third of 60 is 20, and to construct a 20 degree angle you need to construct t = cos 20 degrees. But from trig, t is a root of x^3 - 3 x - 1 (which is irreducible over the rationals), so t has degree 3 --- and 3 is not a power of 2. Hence, a 60 degree angle can't be trisected.

Squaring the circle means given a circle, construct (the side of) a square with the same area. Take the circle to have radius 1, so its area is pi. The square you need would have side pi^(1/2), but pi (and pi^(1/2)) isn't algebraic in the sense noted above. (Lindemann showed pi is transcendental.) So you can't square an arbitrary circle.

Duplicating the cube means given a cube (say with sides of length 1), construct (the side of) a cube whose volume is twice the volume of the original cube (so in this case, the new cube should have volume 2, and its sides should have length 2^(1/3). But 2^(1/3) is a root of the irreducible rational polynomial x^3 -2, so it has degree 3, and again, 3 is not a power of 2.

What's remarkable about this is that, once you prove the theorem (which isn't that hard, just a little fussy), you can dispose of those three old contruction problems so easily.

(Anyone who wants more details - I've left out a lot - can consult any book on Galois theory. Also, Nathan Jacobson's "Basic Algebra I" covers this [https://store.doverpublications.com/0486471896.html] --- it's a classic of abstract algebra which I like a lot, though a little old-fashioned.)

I think this really depends on how much you're willing to assume. You are right of course that the general problem is intractable, because you'd end up having to analyze frameworks, system calls, kernels, etc. But if you are able to assume those function as stated, then yes, you can certainly prove limited facts. For example, the sel4 microkernel is proven correct. Part of this proof of correctness is that all system calls do terminate.

But, actually, the most straightforward way to show that most 'everyday' programs terminate is -- assuming functionality of the language runtime as stated -- that they typically consist of non-recursive functions or functions on structurally smaller inputs. It would be obnoxious, but not difficult to show that a program like 'grep' terminates, assuming functionality of the operating system and hardware on which its running. This is actually fairly straightforwards, and many many functional languages with a focus on correctness have totality checking builtin. For example, Idris and Agda.

Of course, if you're going to ask to prove both functionality of the operating system (like Linux + glibc) or the processor itself, then that could indeed be trickier. But, if you limit your stack, it's certainly possible. The truth is that most computing does not consist of solving Turing complete problems.