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.
That doesn't seem sustainable. It also seems like a poor cost to value ratio.
That doesn't seem sustainable. It also seems like a poor cost to value ratio
Those "prove" you see in academic paper are very specific case.
> 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.
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.
Fully verified programs do exist (e.g. CompCert C compiler), although for various reasons, it's still a niche.