We have figured it out. People with a PhD and given enough time can do it. Scaling this will be possible, especially with the help of AI, as soon as there is the actual will there to do it.

We haven't even figured out how to specify what "correctness" means for all but the most trivial examples. What is the "correct" behavior of that example snippet in the linked post?

I don't know anything about formal correctness proofs but my imagination tells me it is bounded by the description of the task. Aren't we just shifting the bugs toward the task description? Or is it about being able to specify a task with a very simple program (e.g. brute force) that is unfeasible to run but can be somehow used to verify that simpler (in terms of runtime complexity) programs provide the same outputs?

Yes. Figuring out what a program SHOULD do is often as hard as figuring out how to actually do it. The relative difficulty shifts depending how far you are from the real world. The closer your project is to actual people doing actual work, the harder it is to define the requirements precisely.

Yes, they can only logically deduce correctness based on our assumptions of a given system boundary. But I think it is typically a good idea to write them down formally if you need the guarantees. They are also typically smaller and more declarative.

Sure, if your task description/specification is buggy nothing can save you, but if you only have to check the spec your work gets much easier. If you write a program, you have to both make sure that the spec is correct and that the spec is correctly implemented.

Very good question! Try to figure it out yourself and you will see what is wrong with software development today.

So, for people to quickly implement http requests, we need a mountain of AI hardware backed by legions of PhDs with endless time to vet the http requests.

That doesn't seem sustainable. It also seems like a poor cost to value ratio.

No. If it is something that has been done plenty of times before, then we would also know how to prove the correctness of it automatically. It would also lead to much better and less code, because you would be aware that it has been done before so many times.

So, for people to quickly implement http requests, we need to feed, clothe, and discipline humans for a minimum of two decades, backed by legions of teachers, doctors, and professors with endless time to service them.

That doesn't seem sustainable. It also seems like a poor cost to value ratio

Proofing correctness (in general) is incomputible (halting problem and stuffs).

Those "prove" you see in academic paper are very specific case.

Thankfully correctness in the general case doesn't matter in reality, in the same way that it doesn't matter that not all 'correct' programs can be possibly typed.

And I don't know why you put "prove" in scare quotes. There is formally verified software that has been proven to conform to a spec. They aren't just toy programs either, see SEL4 or CompCert for 'real' programs.

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.

> Proofing correctness (in general) is incomputible (halting problem and stuffs).

> Those "prove" you see in academic paper are very specific case.

Not to put too fine a point on it, but every program written is a very specific case, so I'm not sure this is such a convincing point.

As you say, there is absolutely, provably, no general-purpose algorithm out there that will prove program correctness automatically. That is in no way to say that humans can't or shouldn't try to prove some programs correct, or even that you can't have an algorithm that will prove certain classes of programs correct.

With that said, I do also think your parent:

> We have figured it out. People with a PhD and given enough time can do it. Scaling this will be possible, especially with the help of AI, as soon as there is the actual will there to do it.

is too optimistic, and throwing a little cold water on that rosy prediction is appropriate.

I admire your optimism.