[akhosravian]

I’m not a CS academic or a mathematician, but don’t Godel’s incompleteness theorems preclude a formal proof of correctness?

[Verdex]

No.

Godel means that we can't have an algorithmic box that we put a program into and out comes a true/false statement of halting.

Nothing is stopping you from writing the proof manually for each program that you want to prove properties for.

ALSO, you can write sub-turing complete programs. Those are allowed to have automated halting proofs (see idris et al).

[kevindamm]

What you're talking about is actually the Church-Turing thesis and the halting problem.

While, yes, computability and provability are very closely related, it's important to get attribution correct.

More details on what Gödel's Incompleteness Theorem really said are in a sibling comment so I won't repeat them here.

[Verdex]

> it's important to get attribution correct.

Really? Says who?

Or perhaps you'll prove it from first principles. Although if turns out to be difficult, that's okay. Somebody mentioned something about systems being either complete or consistent but never both. Some things can be true but not proveably so. Can't quite remember who it was though.

[kevindamm]

Fair enough, I was being annoyingly pedantic.

[I believe that] it's important to get attribution correct.

[Verdex]

To be fair, annoyingly pedantic is the best kind of pedantic.

- Futurama (kind of)

[kevindamm]

sounds technically correct

Gödel's really was a rather unique mind, and the story of his death is kind of sad.. but I wonder if it takes such a severe kind of paranoia to look for how math can break itself, especially during that time when all the greatest mathematicians were in pursuit of formalizing a complete and consistent mathematics.

[Veserv]

No. It merely prevents you from confirming every arbitrarily complex proof. Incompleteness is more like: I give you a convoluted mess of spaghetti code and claim it computes prime numbers and I demand you try to prove me wrong.

[topaz0]

No. There are plenty of things that can be proved, it's just that there exist true statements that cannot be proved.

[kevindamm]

That's closer, but still not quite right.

There are well-formed statements that can be proved but which assert that its godelized value represents a non-provable theorem.

Therefore, you must accept that it and its contradiction are both provable (leading to an inconsistent system), or not accept it and now there are provable theorems that cannot be expressed in the system.

Furthermore, that this can be constructed from anything with base arithmetic and induction over first-order logic (Gödel's original paper included how broadly it could be applied to basically every logical system).

[kevindamm]

The important thing to note is that it doesn't have anything to do with truth or truth-values of propositions. It breaks the fundamental operation of the provability of a statement.

And, since many proofs are done by assuming a statement's inverse and trying to prove a contradiction, having a known contradiction in the set of provable statements can effectively allow any statement to be proven. Keeping the contradiction is not actually an option.