A software developer with interest in mathemathics, formal systems and undecidability. I like the halting problem and the Gödel incompletness theorems.

I like the fact that you can derive, from the halting problem, a non-constructive meta-proof about the existence of a set of programs that don't halt and also have no non-termination proof. This meta-proof can't be constructive. Therefore, there is a constructive meta-meta-proof about non-constructive proofs that can't be constructive.

I like to conjecture that a program that enumerates ZFC theorems and has the instruction to halt if it finds a P=NP theorem, its negation, or a theorem stating its independence, will never halt. If that is the case, the conjecture could never be proven.