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"
So if I have a language where I can encode in the type system that a number is a prime and is even, then for example the following would be a theorem with a proof:
Lemma even-prime: a -> Prime(a) ∧ Even(a) { // read as 'it returns a number `a` that is both prime and even
return 2
}
So they often have dependent type systems -- in these you can freely mix functions and values in your type signatures, not just types. E.g. you could have a Matrix type with two parameters, and then you can have functions like `transpose: Matrix a b -> Matrix b a`.
---
But this is just one side of the whole thing, the other is how to actually prove anything, like what even is `Even` in the above? A type like `someNum: Int` is also a theorem, but it only translates to "there exists an integer" - hardly interesting.
The real "mind blow" (at least to me) was that we just simply create a type for Equality. It takes the same parameter twice [1] (like in the Matrix example it would be Matrix a a) -- and thus we get a construct that can only be instantiated if the two sides are equal as per the language's compilers rules, that is automatically enforced by the compiler itself!
So now you can have `Eq 2 (1+1)`, but not `Eq 2 (1+3)`. And one last step that makes it general enough for all kinds of proofs, the compiler of these languages are not Turing complete. You can write many things, but for reasoning about loops you usually introduce a fuel that is always decreasing (and thus the compiler will accept it, as it knows it will run out once and that's enough for it). So it can evaluate everything, even in types and creating a normalized expression -- and then accepts everything as equal that normalizes to the same thing.
So for a more complex proof, you can just break down the problem to small steps that are by themselves understandably equal by the compiler.
[1] It's not quite true in this form
Like, they use some pretty stark terms here:
Of course "proving" and "without flaws" are just words in a language game and might not mean the absolute things we expect them to as laypeople. Is that what's going on? Or can the "code" they're "proving... runs correctly" indeed be unrelated to such a fundamental finding of compsci?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. :(