Since code is cheap there is no excuse to not have verification everywhere.
Proving that a particular program will or won't halt can still be easy.
The halting problem does imply that there exist programs which are entirely correct that lean will never be able to prove the correctness of, but this is not really relevant in practice.
On some programs like "stop" or "while(true)" the proof is easy.
With more sophisticated analysers it becomes possible on wider range of programs.
This limits programs to the ones that can be formally shown to terminate. Which is good enough for most purposes.
My approach is to accept programs that run forever as long as I'm fairly sure each loop makes progress of some sort (instead of simply doing "while not solved: continue").
Edit: There's also a fun algorithm that, as far as I know, only provably terminates by being bounded by a sequence of strictly decreasing ordinals. Which breaks all kinds of models for proving it terminates.
answer to the first is same as always - by simply not guaranteeing that everything is provable, especially in finite amount of time
Like, they use some pretty stark terms here:
Formal verification—mathematically proving code runs correctly without flaws—is the highest standard of security assurance; however, it is difficult and often labor-intensive.
I type this message to you all with sadness in my heart, cause I know I could get a better answer 100x faster by just asking an agent to research, which I could then have it dumb down to my level until I grasp it. I don't really know what the point of forums are, anymore. It's undeniably hard not to see ourselves as a planet of sad, fragile monkeys wasting away the hours between birth and death. That was already the case, perhaps, but at least learning and sharing knowledge about engineering in places like this felt like a somewhat meaningful way to positively impact the material conditions of my fellow humans, even in an indirect way. As of November 2026, I'm just the taste/framing component of artificial minds that seem overwhelmingly likely to develop their own within months or maybe years.
For a long time (since noticing the singularity) I've felt like someone doused in napalm and set alight while falling through the sky, frantically trying to put myself out while fixing my broken parachute. But post-Mythos I can't help but fear that there is no solid ground below. Just endless void. :(
The difficulty lies in coming up with the right formulations, and also some times altering the program to make it amenable to proof. It's quite often the case that a proof won't go through unless the program itself has the right idea.
As for the halting problem: it is highly theoretical. Lots of programs which are useful can be proven to halt for instance. Or you can just prove that the program is correct up to the point in time where the sun expansion covers the earth. There are often practical ways around such limitations, including the alteration or reformulation of the program.
the only thing halting problem says is that you can't prove *everything*
feel the difference between "any" and "every"
to stop being able to prove "every" thing you only need to 1 counterexample - which Turing found
all explicit examples of unprovable things are very removed from real demand (other than "prove arbitrary program halts", which probably doesn't count as real demand anyway and more of vapordream)
And just to add, this is also true of "human" mathematics as well.
Why can't ai do this too? Is this the fundamental limit of ai?