What if those programs were guaranteed to do the right thing, if only that had enough time or space to finish? Maybe they're still "correct".

Or, to put it another way: our existing type systems don't make code "provably correct", and when people say that it does (like the commenter above), they're trying to talk you into something.

>our existing type systems don't make code "provably correct"

That is what I am telling you.

>and when people say that it does (like the commenter above)

They said no such thing.

Yes, you're telling me something that I was already trying to demonstrate with my example.

I can't speak to your motive, all I can do is read what you posted. What you posted was wrong, and I explained that.

What I posted was obviously self-contradictory, which is not the same as wrong.

What you posted was wrong, like I said. There are programs that have proofs demonstrating they are free of bugs. You have not seen them do either of the things you claim to have seen. You were stating something false.