3 ms·
The halting problem doesn't prevent you from writing proofs for programs, same as Gödel's theorems don't prevent mathematical proofs from existing. Fully verif
by Tainnor 5y ago
The halting problem doesn't prevent you from writing proofs for programs, same as Gödel's theorems don't prevent mathematical proofs from existing.
Fully verified programs do exist (e.g. CompCert C compiler), although for various reasons, it's still a niche.