Godel’s theorem says that unprovable true statements exist. Fortunately there is a vast set of provable true statements that are quite useful in real life.
Similarly, the halting problem is that you can’t write a program that always determines whether absolutely any program you give it will halt. But in real life compilers can still detect infinite loops in your code unless you try really hard to fool them.
In practical terms a software system can never be “perfect”, because first you have to define “perfect” (i.e., specify correct behavior in every possible state), which is practically impossible, and even if you manage that, the hardware has to implement the software abstraction perfectly, and that never happens. (See prefetch attacks, cache timing attacks, supply glitch attacks, rowhammer, etc.)
The security issues come about when someone finds where you failed to specify desired behavior, or (at any level) your system failed to implement it in some circumstance. No strange loop required.
Having never written compiled code, this intriques me. I often write one offs that I actually want to loop infinitely until I tell them to stop.
How does the compiler know whether it's just really long or infinite? Like, if I write a progressive approximation of pi or prime search algorithm, both are never going to halt because we're certain there are infinite digits of pi and prime numbers. The program could technically halt, but not as a function of the program but rather the hardware.
Or, being silly, if I write a "flip bits in target directory until all bits are flipped" and target /dev/null as a user of the software, it wouldn't halt, so the compiler would detect that?
Is there some --don't-mind-the-recursion flag for developing a program like ycruncher? I get the feeling that there's a list of "this typically causes infinities" that it checks against and if your use isn't on there well then... So it's just the mouse/mouse trap thing but in a compiler?
Or is there some unique CS going on that the compiler employs to determine certain classes of loops?
When you tell it to, you usually have good control around what kind of thing you want it to consider a problem, how much effort you want it to spend trying to prove that, and what should happen with code it can't prove that property for. Most commonly, people just use the "tell me if I've made an obviously dumb infinite loop which does nothing useful while it runs".
E.g. y-cruncher does something other than infinitely loop for no reason so it wouldn't trigger the loop detection logic on most anyone's compilation settings.
On the other hand, a loop which does nothing but run until the last digit of pi would either trigger the compiler to say this is a useless infinite loop or to say it isn't able to prove this loop stops (almost certainly the latter, as such a loop is a great example of going out of your way to fool the compiler).
A loop which sometimes terminates and sometimes doesn't depending on runtime input would depend on your compiler settings, but almost always nobody sets it in a way to say that's a problem (and when they do almost always it's not possible for the compiler to prove one way or the other) if their compiler even supports that kind of analysis.
[0] https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2023/p28...
for(;;) // intentional
for(unsigned i=10;i>=0;i--)
for(int i=0;j<10;i++)
for(unsigned i=0;i!=100;i+=8)
// unintentional
guaranteed termination also is needed for some optimizations. but since side-effect-less infinite loops are UB in C, a compiler doesn't have to prove that such a loop terminates, it can just assume it does. other languages may differ, but I don't think any of them prove convergence of algorithms.
a don't-mind-the-recursion flag can be `-fno-finite-loops` on clang, or a read or write to a `volatile` variable in standard C.
One straightforward approach is to use Hoare logic [1], specifically the method of loop invariants and loop conditions. If you have a loop where the conditions are expressed only in terms of invariants then the conditions will never change truth values during iteration of the loop, thus you have an infinite loop.
Now, some loops are written deliberately like this, i.e. "while (true)", and so there you need to look at whether the body of the loop contains any side effects (reading input, printing, etc). Then you have what is called a "productive infinite loop", such as an event loop or a REPL. Of course you can't prove this sort of loop will ever halt, since the user may never elect to issue the quit command, but these sorts of loops often tend to spend most of their time with the process sleeping until the operating system wakes them up to handle an event.
Another way you have very good (and fake) security, is by reducing the scope of the problem - if you check every request against a very strong crypto signature, it's also practically unbreakable.
But then you have issues like who signs these tokens, who decides which user gets what permissions etc. etc. which mean you have to weaken practical security to make it useful.
Another example is the L4 microkernel, which 'proven' to be bug-free and secure. But it also doesn't do like 99% of the stuff a regular kernel like Linux does, and sort of pushes the issue to the user.
So even defining 'perfect' security in a way that the system remains practically usable is very difficult and potentially impossible.
We come down to to the permissions problem - each person should have as much permissions to do their work as necessary and nothing more - which is essentially a reformulation of Gödel's incompleteness theorem.
Gödel's Incompleteness, very roughly, says that not every true statement (in a formal system) can be proven. In particular, it says that for a logic equipped with arithmetic the statement holds; how you get to security I do not follow.
The idea is that since you can make every security program turing complete, I thiiiiink?, then you can have it be a formal system. So, you can then get the code, in very tortured ways, to execute a paradox, thereby breaking it. Likely in enough ways to let you gain access, though not always.
Clearly our math system gives basic math, so we should conclude that it is either 'incomplete' or broken. Before the incompleteness theorem, it was exciting to imagine that it might be complete, but we had no idea. Now it seems likely to be incomplete. The odds of it being broken haven't really changed.
If it is broken, 2+2 still equals 4 (we didn't really learn that fact from abstract math), but we'll need to fix up set theory. In a world where math isn't formally verified (and even lean itself isn't formally verified), the Incompleteness Theorem is permission to be awed by how huge the space of all logical deduction is, not an argument that logic is a fiction.
To come at it another way, do you believe that there is an 64-bit integer which, any time it is inserted into register 8 on any computer, will immediate convert the raw mass of the earth into a black hole? No, because even if you suspect there is a hole in the foundation of math, you still believe in brute-force case-analysis, and you know that every 64-bit integer has been inserted into register 8 on a computer before.
But yes, a hard recommendation. Absolutely worth the time. It's also pretty easy to read.